pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[inferbo] Use big_int in interval domain

Browse Source 
Summary: It uses big int, instead of 63bits int of OCaml, in the interval domain in order to get preciser numeric values in the future.

Reviewed By: jvillard

Differential Revision: D10123364

fbshipit-source-id: c217f4366
master
Sungkeun Cho 6 years ago committed by Facebook Github Bot
parent cd49a0c72d
commit 96cbdb15c7
16 changed files with 273 additions and 200 deletions
Show Stats Download Patch File Download Diff File

2
infer/src/IR/IntLit.ml
Unescape View File

@ -63,6 +63,8 @@ let to_int (_, i, _) = Int64.to_int i
let to_int_exn (_, i, _) = Int64.to_int_exn i let to_int_exn (_, i, _) = Int64.to_int_exn i
let to_big_int (_, i, _) = Z.of_int64 i
let to_float (_, i, _) = Int64.to_float i let to_float (_, i, _) = Int64.to_float i
let null = (false, 0L, true) let null = (false, 0L, true)

2
infer/src/IR/IntLit.mli
Unescape View File

@ -91,6 +91,8 @@ val to_int : t -> int option
val to_int_exn : t -> int val to_int_exn : t -> int
val to_big_int : t -> Z.t
val to_float : t -> float val to_float : t -> float
val to_signed : t -> t option val to_signed : t -> t option

224
infer/src/bufferoverrun/bounds.ml
Unescape View File

@ -42,9 +42,9 @@ module SymLinear = struct
let le : t -> t -> bool = let le : t -> t -> bool =
fun x y -> fun x y ->
let le_one_pair s v1_opt v2_opt = let le_one_pair s v1_opt v2_opt =
let v1 = NonZeroInt.opt_to_int v1_opt in let v1 = NonZeroInt.opt_to_big_int v1_opt in
let v2 = NonZeroInt.opt_to_int v2_opt in let v2 = NonZeroInt.opt_to_big_int v2_opt in
Int.equal v1 v2 || (Symb.Symbol.is_unsigned s && v1 <= v2) Z.(equal v1 v2) || (Symb.Symbol.is_unsigned s && v1 <= v2)
in in
M.for_all2 ~f:le_one_pair x y M.for_all2 ~f:le_one_pair x y
@ -64,17 +64,17 @@ module SymLinear = struct
let eq : t -> t -> bool = let eq : t -> t -> bool =
fun x y -> fun x y ->
let eq_pair _ (coeff1 : NonZeroInt.t option) (coeff2 : NonZeroInt.t option) = let eq_pair _ (coeff1 : NonZeroInt.t option) (coeff2 : NonZeroInt.t option) =
[%compare.equal: int option] (coeff1 :> int option) (coeff2 :> int option) [%compare.equal: Z.t option] (coeff1 :> Z.t option) (coeff2 :> Z.t option)
in in
M.for_all2 ~f:eq_pair x y M.for_all2 ~f:eq_pair x y
let pp1 : F.formatter -> Symb.Symbol.t * NonZeroInt.t -> unit = let pp1 : F.formatter -> Symb.Symbol.t * NonZeroInt.t -> unit =
fun fmt (s, c) -> fun fmt (s, c) ->
let c = (c :> int) in let c = (c :> Z.t) in
if Int.equal c 1 then Symb.Symbol.pp fmt s if Z.(equal c one) then Symb.Symbol.pp fmt s
else if Int.equal c (-1) then F.fprintf fmt "-%a" Symb.Symbol.pp s else if Z.(equal c minus_one) then F.fprintf fmt "-%a" Symb.Symbol.pp s
else F.fprintf fmt "%dx%a" c Symb.Symbol.pp s else F.fprintf fmt "%ax%a" Z.pp_print c Symb.Symbol.pp s
let pp : F.formatter -> t -> unit = let pp : F.formatter -> t -> unit =
@ -106,7 +106,7 @@ module SymLinear = struct
let one_symbol_of_coeff : NonZeroInt.t -> t -> Symb.Symbol.t option = let one_symbol_of_coeff : NonZeroInt.t -> t -> Symb.Symbol.t option =
fun coeff x -> fun coeff x ->
match M.is_singleton x with match M.is_singleton x with
| Some (k, v) when Int.equal (v :> int) (coeff :> int) -> | Some (k, v) when Z.equal (v :> Z.t) (coeff :> Z.t) ->
Some k Some k
| _ -> | _ ->
None None
@ -153,9 +153,9 @@ module SymLinear = struct
(* we can give integer bounds (obviously 0) only when all symbols are unsigned *) (* we can give integer bounds (obviously 0) only when all symbols are unsigned *)
let int_lb x = if is_ge_zero x then Some 0 else None let big_int_lb x = if is_ge_zero x then Some Z.zero else None
let int_ub x = if is_le_zero x then Some 0 else None let big_int_ub x = if is_le_zero x then Some Z.zero else None
(** When two following symbols are from the same path, simplify what would lead to a zero sum. E.g. 2 * x.lb - x.ub = x.lb *) (** When two following symbols are from the same path, simplify what would lead to a zero sum. E.g. 2 * x.lb - x.ub = x.lb *)
let simplify_bound_ends_from_paths : t -> t = let simplify_bound_ends_from_paths : t -> t =
@ -198,7 +198,7 @@ module Bound = struct
let neg = function Plus -> Minus | Minus -> Plus let neg = function Plus -> Minus | Minus -> Plus
let eval_int x i1 i2 = match x with Plus -> i1 + i2 | Minus -> i1 - i2 let eval_big_int x i1 i2 = match x with Plus -> Z.(i1 + i2) | Minus -> Z.(i1 - i2)
let pp ~need_plus : F.formatter -> t -> unit = let pp ~need_plus : F.formatter -> t -> unit =
fun fmt -> function fun fmt -> function
@ -217,7 +217,7 @@ module Bound = struct
let neg = function Min -> Max | Max -> Min let neg = function Min -> Max | Max -> Min
let eval_int x i1 i2 = match x with Min -> min i1 i2 | Max -> max i1 i2 let eval_big_int x i1 i2 = match x with Min -> Z.min i1 i2 | Max -> Z.max i1 i2
let pp : F.formatter -> t -> unit = let pp : F.formatter -> t -> unit =
fun fmt -> function Min -> F.pp_print_string fmt "min" | Max -> F.pp_print_string fmt "max" fun fmt -> function Min -> F.pp_print_string fmt "min" | Max -> F.pp_print_string fmt "max"
@ -227,8 +227,8 @@ module Bound = struct
e.g. `MinMax (1, Minus, Max, 2, s)` means "1 - max (2, s)". *) e.g. `MinMax (1, Minus, Max, 2, s)` means "1 - max (2, s)". *)
type t = type t =
| MInf | MInf
| Linear of int * SymLinear.t | Linear of Z.t * SymLinear.t
| MinMax of int * Sign.t * MinMax.t * int * Symb.Symbol.t | MinMax of Z.t * Sign.t * MinMax.t * Z.t * Symb.Symbol.t
| PInf | PInf
[@@deriving compare] [@@deriving compare]
@ -241,24 +241,26 @@ module Bound = struct
| PInf -> | PInf ->
F.pp_print_string fmt "+oo" F.pp_print_string fmt "+oo"
| Linear (c, x) -> | Linear (c, x) ->
if SymLinear.is_zero x then F.pp_print_int fmt c if SymLinear.is_zero x then Z.pp_print fmt c
else if Int.equal c 0 then SymLinear.pp fmt x else if Z.(equal c zero) then SymLinear.pp fmt x
else F.fprintf fmt "%a + %d" SymLinear.pp x c else F.fprintf fmt "%a + %a" SymLinear.pp x Z.pp_print c
| MinMax (c, sign, m, d, x) -> | MinMax (c, sign, m, d, x) ->
if Int.equal c 0 then (Sign.pp ~need_plus:false) fmt sign if Z.(equal c zero) then (Sign.pp ~need_plus:false) fmt sign
else F.fprintf fmt "%d%a" c (Sign.pp ~need_plus:true) sign ; else F.fprintf fmt "%a%a" Z.pp_print c (Sign.pp ~need_plus:true) sign ;
F.fprintf fmt "%a(%d, %a)" MinMax.pp m d Symb.Symbol.pp x F.fprintf fmt "%a(%a, %a)" MinMax.pp m Z.pp_print d Symb.Symbol.pp x
let of_bound_end = function Symb.BoundEnd.LowerBound -> MInf | Symb.BoundEnd.UpperBound -> PInf let of_bound_end = function Symb.BoundEnd.LowerBound -> MInf | Symb.BoundEnd.UpperBound -> PInf
let of_int : int -> t = fun n -> Linear (n, SymLinear.empty) let of_int : int -> t = fun n -> Linear (Z.of_int n, SymLinear.empty)
let of_big_int : Z.t -> t = fun n -> Linear (n, SymLinear.empty)
let minus_one = of_int (-1) let minus_one = of_int (-1)
let _255 = of_int 255 let _255 = of_int 255
let of_sym : SymLinear.t -> t = fun s -> Linear (0, s) let of_sym : SymLinear.t -> t = fun s -> Linear (Z.zero, s)
let is_symbolic : t -> bool = function let is_symbolic : t -> bool = function
| MInf | PInf -> | MInf | PInf ->
@ -270,7 +272,7 @@ module Bound = struct
let lift_symlinear : (SymLinear.t -> 'a option) -> t -> 'a option = let lift_symlinear : (SymLinear.t -> 'a option) -> t -> 'a option =
fun f -> function Linear (0, se) -> f se | _ -> None fun f -> function Linear (n, se) when Z.(equal n zero) -> f se | _ -> None
let get_one_symbol_opt : t -> Symb.Symbol.t option = lift_symlinear SymLinear.get_one_symbol_opt let get_one_symbol_opt : t -> Symb.Symbol.t option = lift_symlinear SymLinear.get_one_symbol_opt
@ -292,10 +294,10 @@ module Bound = struct
let is_mone_symbol : t -> bool = fun x -> get_mone_symbol_opt x <> None let is_mone_symbol : t -> bool = fun x -> get_mone_symbol_opt x <> None
let mk_MinMax (c, sign, m, d, s) = let mk_MinMax (c, sign, m, d, s) =
if Symb.Symbol.is_unsigned s && d <= 0 then if Symb.Symbol.is_unsigned s && Z.(d <= zero) then
match m with match m with
| Min -> | Min ->
of_int (Sign.eval_int sign c d) of_big_int (Sign.eval_big_int sign c d)
| Max -> ( | Max -> (
match sign with match sign with
| Plus -> | Plus ->
@ -305,59 +307,59 @@ module Bound = struct
else MinMax (c, sign, m, d, s) else MinMax (c, sign, m, d, s)
let int_ub_of_minmax = function let big_int_ub_of_minmax = function
| MinMax (c, Plus, Min, d, _) -> | MinMax (c, Plus, Min, d, _) ->
Some (c + d) Some Z.(c + d)
| MinMax (c, Minus, Max, d, s) when Symb.Symbol.is_unsigned s -> | MinMax (c, Minus, Max, d, s) when Symb.Symbol.is_unsigned s ->
Some (min c (c - d)) Some Z.(min c (c - d))
| MinMax (c, Minus, Max, d, _) -> | MinMax (c, Minus, Max, d, _) ->
Some (c - d) Some Z.(c - d)
| MinMax _ -> | MinMax _ ->
None None
| MInf | PInf | Linear _ -> | MInf | PInf | Linear _ ->
assert false assert false
let int_lb_of_minmax = function let big_int_lb_of_minmax = function
| MinMax (c, Plus, Max, d, s) when Symb.Symbol.is_unsigned s -> | MinMax (c, Plus, Max, d, s) when Symb.Symbol.is_unsigned s ->
Some (max c (c + d)) Some Z.(max c (c + d))
| MinMax (c, Plus, Max, d, _) -> | MinMax (c, Plus, Max, d, _) ->
Some (c + d) Some Z.(c + d)
| MinMax (c, Minus, Min, d, _) -> | MinMax (c, Minus, Min, d, _) ->
Some (c - d) Some Z.(c - d)
| MinMax _ -> | MinMax _ ->
None None
| MInf | PInf | Linear _ -> | MInf | PInf | Linear _ ->
assert false assert false
let int_of_minmax = function let big_int_of_minmax = function
| Symb.BoundEnd.LowerBound -> | Symb.BoundEnd.LowerBound ->
int_lb_of_minmax big_int_lb_of_minmax
| Symb.BoundEnd.UpperBound -> | Symb.BoundEnd.UpperBound ->
int_ub_of_minmax big_int_ub_of_minmax
let int_lb = function let big_int_lb = function
| MInf -> | MInf ->
None None
| PInf -> | PInf ->
assert false assert false
| MinMax _ as b -> | MinMax _ as b ->
int_lb_of_minmax b big_int_lb_of_minmax b
| Linear (c, se) -> | Linear (c, se) ->
SymLinear.int_lb se |> Option.map ~f:(( + ) c) SymLinear.big_int_lb se |> Option.map ~f:(Z.( + ) c)
let int_ub = function let big_int_ub = function
| MInf -> | MInf ->
assert false assert false
| PInf -> | PInf ->
None None
| MinMax _ as b -> | MinMax _ as b ->
int_ub_of_minmax b big_int_ub_of_minmax b
| Linear (c, se) -> | Linear (c, se) ->
SymLinear.int_ub se |> Option.map ~f:(( + ) c) SymLinear.big_int_ub se |> Option.map ~f:(Z.( + ) c)
let linear_ub_of_minmax = function let linear_ub_of_minmax = function
@ -383,7 +385,11 @@ module Bound = struct
let le_minmax_by_int x y = let le_minmax_by_int x y =
match (int_ub_of_minmax x, int_lb_of_minmax y) with Some n, Some m -> n <= m | _, _ -> false match (big_int_ub_of_minmax x, big_int_lb_of_minmax y) with
| Some n, Some m ->
n <= m
| _, _ ->
false
let le_opt1 le opt_n m = Option.value_map opt_n ~default:false ~f:(fun n -> le n m) let le_opt1 le opt_n m = Option.value_map opt_n ~default:false ~f:(fun n -> le n m)
@ -401,17 +407,17 @@ module Bound = struct
c0 <= c1 && SymLinear.le x0 x1 c0 <= c1 && SymLinear.le x0 x1
| MinMax (c1, sign1, m1, d1, x1), MinMax (c2, sign2, m2, d2, x2) | MinMax (c1, sign1, m1, d1, x1), MinMax (c2, sign2, m2, d2, x2)
when Sign.equal sign1 sign2 && MinMax.equal m1 m2 -> when Sign.equal sign1 sign2 && MinMax.equal m1 m2 ->
c1 <= c2 && Int.equal d1 d2 && Symb.Symbol.equal x1 x2 c1 <= c2 && Z.equal d1 d2 && Symb.Symbol.equal x1 x2
| MinMax _, MinMax _ when le_minmax_by_int x y -> | MinMax _, MinMax _ when le_minmax_by_int x y ->
true true
| MinMax (c1, Plus, Min, _, x1), MinMax (c2, Plus, Max, _, x2) | MinMax (c1, Plus, Min, _, x1), MinMax (c2, Plus, Max, _, x2)
| MinMax (c1, Minus, Max, _, x1), MinMax (c2, Minus, Min, _, x2) -> | MinMax (c1, Minus, Max, _, x1), MinMax (c2, Minus, Min, _, x2) ->
c1 <= c2 && Symb.Symbol.equal x1 x2 c1 <= c2 && Symb.Symbol.equal x1 x2
| MinMax _, Linear (c, se) -> | MinMax _, Linear (c, se) ->
(SymLinear.is_ge_zero se && le_opt1 Int.( <= ) (int_ub_of_minmax x) c) (SymLinear.is_ge_zero se && le_opt1 Z.leq (big_int_ub_of_minmax x) c)
|| le_opt1 le (linear_ub_of_minmax x) y || le_opt1 le (linear_ub_of_minmax x) y
| Linear (c, se), MinMax _ -> | Linear (c, se), MinMax _ ->
(SymLinear.is_le_zero se && le_opt2 Int.( <= ) c (int_lb_of_minmax y)) (SymLinear.is_le_zero se && le_opt2 Z.leq c (big_int_lb_of_minmax y))
|| le_opt2 le x (linear_lb_of_minmax y) || le_opt2 le x (linear_lb_of_minmax y)
| _, _ -> | _, _ ->
false false
@ -423,9 +429,9 @@ module Bound = struct
| MInf, Linear _ | MInf, MinMax _ | MInf, PInf | Linear _, PInf | MinMax _, PInf -> | MInf, Linear _ | MInf, MinMax _ | MInf, PInf | Linear _, PInf | MinMax _, PInf ->
true true
| Linear (c, x), _ -> | Linear (c, x), _ ->
le (Linear (c + 1, x)) y le (Linear (Z.succ c, x)) y
| MinMax (c, sign, min_max, d, x), _ -> | MinMax (c, sign, min_max, d, x), _ ->
le (mk_MinMax (c + 1, sign, min_max, d, x)) y le (mk_MinMax (Z.succ c, sign, min_max, d, x)) y
| _, _ -> | _, _ ->
false false
@ -454,31 +460,31 @@ module Bound = struct
else else
match (x, y) with match (x, y) with
| Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_one_symbol x2 -> | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_one_symbol x2 ->
mk_MinMax (c2, Plus, Min, c1 - c2, SymLinear.get_one_symbol x2) mk_MinMax (c2, Plus, Min, Z.(c1 - c2), SymLinear.get_one_symbol x2)
| Linear (c1, x1), Linear (c2, x2) when SymLinear.is_one_symbol x1 && SymLinear.is_zero x2 -> | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_one_symbol x1 && SymLinear.is_zero x2 ->
mk_MinMax (c1, Plus, Min, c2 - c1, SymLinear.get_one_symbol x1) mk_MinMax (c1, Plus, Min, Z.(c2 - c1), SymLinear.get_one_symbol x1)
| Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_mone_symbol x2 | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_mone_symbol x2
-> ->
mk_MinMax (c2, Minus, Max, c2 - c1, SymLinear.get_mone_symbol x2) mk_MinMax (c2, Minus, Max, Z.(c2 - c1), SymLinear.get_mone_symbol x2)
| Linear (c1, x1), Linear (c2, x2) when SymLinear.is_mone_symbol x1 && SymLinear.is_zero x2 | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_mone_symbol x1 && SymLinear.is_zero x2
-> ->
mk_MinMax (c1, Minus, Max, c1 - c2, SymLinear.get_mone_symbol x1) mk_MinMax (c1, Minus, Max, Z.(c1 - c2), SymLinear.get_mone_symbol x1)
| MinMax (c1, Plus, Min, d1, s), Linear (c2, se) | MinMax (c1, Plus, Min, d1, s), Linear (c2, se)
| Linear (c2, se), MinMax (c1, Plus, Min, d1, s) | Linear (c2, se), MinMax (c1, Plus, Min, d1, s)
when SymLinear.is_zero se -> when SymLinear.is_zero se ->
mk_MinMax (c1, Plus, Min, min d1 (c2 - c1), s) mk_MinMax (c1, Plus, Min, Z.(min d1 (c2 - c1)), s)
| MinMax (c1, Plus, Max, _, s), Linear (c2, se) | MinMax (c1, Plus, Max, _, s), Linear (c2, se)
| Linear (c2, se), MinMax (c1, Plus, Max, _, s) | Linear (c2, se), MinMax (c1, Plus, Max, _, s)
when SymLinear.is_zero se -> when SymLinear.is_zero se ->
mk_MinMax (c1, Plus, Min, c2 - c1, s) mk_MinMax (c1, Plus, Min, Z.(c2 - c1), s)
| MinMax (c1, Minus, Min, _, s), Linear (c2, se) | MinMax (c1, Minus, Min, _, s), Linear (c2, se)
| Linear (c2, se), MinMax (c1, Minus, Min, _, s) | Linear (c2, se), MinMax (c1, Minus, Min, _, s)
when SymLinear.is_zero se -> when SymLinear.is_zero se ->
mk_MinMax (c1, Minus, Max, c1 - c2, s) mk_MinMax (c1, Minus, Max, Z.(c1 - c2), s)
| MinMax (c1, Minus, Max, d1, s), Linear (c2, se) | MinMax (c1, Minus, Max, d1, s), Linear (c2, se)
| Linear (c2, se), MinMax (c1, Minus, Max, d1, s) | Linear (c2, se), MinMax (c1, Minus, Max, d1, s)
when SymLinear.is_zero se -> when SymLinear.is_zero se ->
mk_MinMax (c1, Minus, Max, max d1 (c1 - c2), s) mk_MinMax (c1, Minus, Max, Z.(max d1 (c1 - c2)), s)
| MinMax (_, Plus, Min, _, _), MinMax (_, Plus, Max, _, _) | MinMax (_, Plus, Min, _, _), MinMax (_, Plus, Max, _, _)
| MinMax (_, Plus, Min, _, _), MinMax (_, Minus, Min, _, _) | MinMax (_, Plus, Min, _, _), MinMax (_, Minus, Min, _, _)
| MinMax (_, Minus, Max, _, _), MinMax (_, Plus, Max, _, _) | MinMax (_, Minus, Max, _, _), MinMax (_, Plus, Max, _, _)
@ -490,7 +496,7 @@ module Bound = struct
| MinMax (_, Minus, Min, _, _), MinMax (_, Minus, Max, _, _) -> | MinMax (_, Minus, Min, _, _), MinMax (_, Minus, Max, _, _) ->
lb ~default (remove_max_int x) y lb ~default (remove_max_int x) y
| MinMax (c1, Plus, Max, d1, _), MinMax (c2, Plus, Max, d2, _) -> | MinMax (c1, Plus, Max, d1, _), MinMax (c2, Plus, Max, d2, _) ->
Linear (min (c1 + d1) (c2 + d2), SymLinear.zero) Linear (Z.(min (c1 + d1) (c2 + d2)), SymLinear.zero)
| _, _ -> | _, _ ->
default default
@ -513,15 +519,15 @@ module Bound = struct
else else
match (x, y) with match (x, y) with
| Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_one_symbol x2 -> | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_one_symbol x2 ->
mk_MinMax (c2, Plus, Max, c1 - c2, SymLinear.get_one_symbol x2) mk_MinMax (c2, Plus, Max, Z.(c1 - c2), SymLinear.get_one_symbol x2)
| Linear (c1, x1), Linear (c2, x2) when SymLinear.is_one_symbol x1 && SymLinear.is_zero x2 -> | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_one_symbol x1 && SymLinear.is_zero x2 ->
mk_MinMax (c1, Plus, Max, c2 - c1, SymLinear.get_one_symbol x1) mk_MinMax (c1, Plus, Max, Z.(c2 - c1), SymLinear.get_one_symbol x1)
| Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_mone_symbol x2 | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_zero x1 && SymLinear.is_mone_symbol x2
-> ->
mk_MinMax (c2, Minus, Min, c2 - c1, SymLinear.get_mone_symbol x2) mk_MinMax (c2, Minus, Min, Z.(c2 - c1), SymLinear.get_mone_symbol x2)
| Linear (c1, x1), Linear (c2, x2) when SymLinear.is_mone_symbol x1 && SymLinear.is_zero x2 | Linear (c1, x1), Linear (c2, x2) when SymLinear.is_mone_symbol x1 && SymLinear.is_zero x2
-> ->
mk_MinMax (c1, Minus, Min, c1 - c2, SymLinear.get_mone_symbol x1) mk_MinMax (c1, Minus, Min, Z.(c1 - c2), SymLinear.get_mone_symbol x1)
| _, _ -> | _, _ ->
default default
@ -534,10 +540,10 @@ module Bound = struct
| PInf, _ | _, PInf -> | PInf, _ | _, PInf ->
L.(die InternalError) "Lower bound cannot be +oo." L.(die InternalError) "Lower bound cannot be +oo."
| MinMax (n1, Plus, Max, _, s1), Linear (n2, s2) | MinMax (n1, Plus, Max, _, s1), Linear (n2, s2)
when Int.equal n1 n2 && SymLinear.is_one_symbol_of s1 s2 -> when Z.equal n1 n2 && SymLinear.is_one_symbol_of s1 s2 ->
y y
| MinMax (n1, Minus, Min, _, s1), Linear (n2, s2) | MinMax (n1, Minus, Min, _, s1), Linear (n2, s2)
when Int.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 -> when Z.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 ->
y y
| _ -> | _ ->
if le x y then x else MInf if le x y then x else MInf
@ -549,28 +555,28 @@ module Bound = struct
| MInf, _ | _, MInf -> | MInf, _ | _, MInf ->
L.(die InternalError) "Upper bound cannot be -oo." L.(die InternalError) "Upper bound cannot be -oo."
| MinMax (n1, Plus, Min, _, s1), Linear (n2, s2) | MinMax (n1, Plus, Min, _, s1), Linear (n2, s2)
when Int.equal n1 n2 && SymLinear.is_one_symbol_of s1 s2 -> when Z.equal n1 n2 && SymLinear.is_one_symbol_of s1 s2 ->
y y
| MinMax (n1, Minus, Max, _, s1), Linear (n2, s2) | MinMax (n1, Minus, Max, _, s1), Linear (n2, s2)
when Int.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 -> when Z.equal n1 n2 && SymLinear.is_mone_symbol_of s1 s2 ->
y y
| _ -> | _ ->
if le y x then x else PInf if le y x then x else PInf
let zero : t = Linear (0, SymLinear.zero) let zero : t = Linear (Z.zero, SymLinear.zero)
let one : t = Linear (1, SymLinear.zero) let one : t = Linear (Z.one, SymLinear.zero)
let mone : t = Linear (-1, SymLinear.zero) let mone : t = Linear (Z.minus_one, SymLinear.zero)
let is_some_const : int -> t -> bool = let is_some_const : Z.t -> t -> bool =
fun c x -> match x with Linear (c', y) -> Int.equal c c' && SymLinear.is_zero y | _ -> false fun c x -> match x with Linear (c', y) -> Z.equal c c' && SymLinear.is_zero y | _ -> false
let is_zero : t -> bool = is_some_const 0 let is_zero : t -> bool = is_some_const Z.zero
let is_const : t -> int option = let is_const : t -> Z.t option =
fun x -> match x with Linear (c, y) when SymLinear.is_zero y -> Some c | _ -> None fun x -> match x with Linear (c, y) when SymLinear.is_zero y -> Some c | _ -> None
@ -582,11 +588,11 @@ module Bound = struct
| _, _ when is_zero y -> | _, _ when is_zero y ->
x x
| Linear (c1, x1), Linear (c2, x2) -> | Linear (c1, x1), Linear (c2, x2) ->
Linear (c1 + c2, SymLinear.plus x1 x2) Linear (Z.(c1 + c2), SymLinear.plus x1 x2)
| MinMax (c1, sign, min_max, d1, x1), Linear (c2, x2) | MinMax (c1, sign, min_max, d1, x1), Linear (c2, x2)
| Linear (c2, x2), MinMax (c1, sign, min_max, d1, x1) | Linear (c2, x2), MinMax (c1, sign, min_max, d1, x1)
when SymLinear.is_zero x2 -> when SymLinear.is_zero x2 ->
mk_MinMax (c1 + c2, sign, min_max, d1, x1) mk_MinMax (Z.(c1 + c2), sign, min_max, d1, x1)
| _ -> | _ ->
f x y f x y
@ -596,10 +602,10 @@ module Bound = struct
match (x, y) with match (x, y) with
| MinMax (c1, Plus, Max, d1, _), Linear (c2, x2) | MinMax (c1, Plus, Max, d1, _), Linear (c2, x2)
| Linear (c2, x2), MinMax (c1, Plus, Max, d1, _) -> | Linear (c2, x2), MinMax (c1, Plus, Max, d1, _) ->
Linear (c1 + d1 + c2, x2) Linear (Z.(c1 + d1 + c2), x2)
| MinMax (c1, Minus, Min, d1, _), Linear (c2, x2) | MinMax (c1, Minus, Min, d1, _), Linear (c2, x2)
| Linear (c2, x2), MinMax (c1, Minus, Min, d1, _) -> | Linear (c2, x2), MinMax (c1, Minus, Min, d1, _) ->
Linear (c1 - d1 + c2, x2) Linear (Z.(c1 - d1 + c2), x2)
| _, _ -> | _, _ ->
MInf ) MInf )
@ -609,10 +615,10 @@ module Bound = struct
match (x, y) with match (x, y) with
| MinMax (c1, Plus, Min, d1, _), Linear (c2, x2) | MinMax (c1, Plus, Min, d1, _), Linear (c2, x2)
| Linear (c2, x2), MinMax (c1, Plus, Min, d1, _) -> | Linear (c2, x2), MinMax (c1, Plus, Min, d1, _) ->
Linear (c1 + d1 + c2, x2) Linear (Z.(c1 + d1 + c2), x2)
| MinMax (c1, Minus, Max, d1, _), Linear (c2, x2) | MinMax (c1, Minus, Max, d1, _), Linear (c2, x2)
| Linear (c2, x2), MinMax (c1, Minus, Max, d1, _) -> | Linear (c2, x2), MinMax (c1, Minus, Max, d1, _) ->
Linear (c1 - d1 + c2, x2) Linear (Z.(c1 - d1 + c2), x2)
| _, _ -> | _, _ ->
PInf ) PInf )
@ -627,15 +633,19 @@ module Bound = struct
| PInf -> | PInf ->
if NonZeroInt.is_positive n then PInf else MInf if NonZeroInt.is_positive n then PInf else MInf
| Linear (c, x') -> | Linear (c, x') ->
Linear (c * (n :> int), SymLinear.mult_const n x') Linear (Z.(c * (n :> Z.t)), SymLinear.mult_const n x')
| MinMax _ -> ( | MinMax _ -> (
let int_bound = let int_bound =
let bound_end' = let bound_end' =
if NonZeroInt.is_positive n then bound_end else Symb.BoundEnd.neg bound_end if NonZeroInt.is_positive n then bound_end else Symb.BoundEnd.neg bound_end
in in
int_of_minmax bound_end' x big_int_of_minmax bound_end' x
in in
match int_bound with Some i -> of_int (i * (n :> int)) | None -> of_bound_end bound_end ) match int_bound with
| Some i ->
of_big_int Z.(i * (n :> Z.t))
| None ->
of_bound_end bound_end )
let mult_const_l = mult_const Symb.BoundEnd.LowerBound let mult_const_l = mult_const Symb.BoundEnd.LowerBound
@ -648,9 +658,9 @@ module Bound = struct
| PInf -> | PInf ->
MInf MInf
| Linear (c, x) -> | Linear (c, x) ->
Linear (-c, SymLinear.neg x) Linear (Z.neg c, SymLinear.neg x)
| MinMax (c, sign, min_max, d, x) -> | MinMax (c, sign, min_max, d, x) ->
mk_MinMax (-c, Sign.neg sign, min_max, d, x) mk_MinMax (Z.neg c, Sign.neg sign, min_max, d, x)
let div_const : t -> NonZeroInt.t -> t option = let div_const : t -> NonZeroInt.t -> t option =
@ -663,7 +673,7 @@ module Bound = struct
| Linear (c, x') when NonZeroInt.is_multiple c n -> ( | Linear (c, x') when NonZeroInt.is_multiple c n -> (
match SymLinear.exact_div_const_exn x' n with match SymLinear.exact_div_const_exn x' n with
| x'' -> | x'' ->
Some (Linear (c / (n :> int), x'')) Some (Linear (Z.(c / (n :> Z.t)), x''))
| exception NonZeroInt.DivisionNotExact -> | exception NonZeroInt.DivisionNotExact ->
None ) None )
| _ -> | _ ->
@ -738,13 +748,13 @@ module Bound = struct
NonBottom x NonBottom x
| Linear (c, se) -> | Linear (c, se) ->
SymLinear.fold se SymLinear.fold se
~init:(NonBottom (of_int c)) ~init:(NonBottom (of_big_int c))
~f:(fun acc s coeff -> lift2 (plus subst_pos) acc (get_mult_const s coeff)) ~f:(fun acc s coeff -> lift2 (plus subst_pos) acc (get_mult_const s coeff))
| MinMax (c, sign, min_max, d, s) -> ( | MinMax (c, sign, min_max, d, s) -> (
match get s with match get s with
| Bottom -> | Bottom ->
Option.value_map (int_of_minmax subst_pos x) ~default:Bottom ~f:(fun i -> Option.value_map (big_int_of_minmax subst_pos x) ~default:Bottom ~f:(fun i ->
NonBottom (of_int i) ) NonBottom (of_big_int i) )
| NonBottom x' -> | NonBottom x' ->
let res = let res =
match (sign, min_max, x') with match (sign, min_max, x') with
@ -753,44 +763,48 @@ module Bound = struct
| Plus, Max, PInf | Minus, Min, MInf -> | Plus, Max, PInf | Minus, Min, MInf ->
PInf PInf
| sign, Min, PInf | sign, Max, MInf -> | sign, Min, PInf | sign, Max, MInf ->
of_int (Sign.eval_int sign c d) of_big_int (Sign.eval_big_int sign c d)
| _, _, Linear (c2, se) -> ( | _, _, Linear (c2, se) -> (
if SymLinear.is_zero se then if SymLinear.is_zero se then
of_int (Sign.eval_int sign c (MinMax.eval_int min_max d c2)) of_big_int (Sign.eval_big_int sign c (MinMax.eval_big_int min_max d c2))
else if SymLinear.is_one_symbol se then else if SymLinear.is_one_symbol se then
mk_MinMax mk_MinMax
(Sign.eval_int sign c c2, sign, min_max, d - c2, SymLinear.get_one_symbol se) ( Sign.eval_big_int sign c c2
, sign
, min_max
, Z.(d - c2)
, SymLinear.get_one_symbol se )
else if SymLinear.is_mone_symbol se then else if SymLinear.is_mone_symbol se then
mk_MinMax mk_MinMax
( Sign.eval_int sign c c2 ( Sign.eval_big_int sign c c2
, Sign.neg sign , Sign.neg sign
, MinMax.neg min_max , MinMax.neg min_max
, c2 - d , Z.(c2 - d)
, SymLinear.get_mone_symbol se ) , SymLinear.get_mone_symbol se )
else else
match int_of_minmax subst_pos x with match big_int_of_minmax subst_pos x with
| Some i -> | Some i ->
of_int i of_big_int i
| None -> | None ->
of_bound_end subst_pos ) of_bound_end subst_pos )
| _, _, MinMax (c2, sign2, min_max2, d2, s2) -> ( | _, _, MinMax (c2, sign2, min_max2, d2, s2) -> (
match (min_max, sign2, min_max2) with match (min_max, sign2, min_max2) with
| Min, Plus, Min | Max, Plus, Max -> | Min, Plus, Min | Max, Plus, Max ->
let c' = Sign.eval_int sign c c2 in let c' = Sign.eval_big_int sign c c2 in
let d' = MinMax.eval_int min_max (d - c2) d2 in let d' = MinMax.eval_big_int min_max Z.(d - c2) d2 in
mk_MinMax (c', sign, min_max, d', s2) mk_MinMax (c', sign, min_max, d', s2)
| Min, Minus, Max | Max, Minus, Min -> | Min, Minus, Max | Max, Minus, Min ->
let c' = Sign.eval_int sign c c2 in let c' = Sign.eval_big_int sign c c2 in
let d' = MinMax.eval_int min_max2 (c2 - d) d2 in let d' = MinMax.eval_big_int min_max2 Z.(c2 - d) d2 in
mk_MinMax (c', Sign.neg sign, min_max2, d', s2) mk_MinMax (c', Sign.neg sign, min_max2, d', s2)
| _ -> | _ ->
let bound_end = let bound_end =
match sign with Plus -> subst_pos | Minus -> Symb.BoundEnd.neg subst_pos match sign with Plus -> subst_pos | Minus -> Symb.BoundEnd.neg subst_pos
in in
of_int of_big_int
(Sign.eval_int sign c (Sign.eval_big_int sign c
(MinMax.eval_int min_max d (MinMax.eval_big_int min_max d
(int_of_minmax bound_end x' |> Option.value ~default:d))) ) (big_int_of_minmax bound_end x' |> Option.value ~default:d))) )
in in
NonBottom res ) NonBottom res )
@ -810,7 +824,7 @@ module Bound = struct
let is_same_symbol b1 b2 = let is_same_symbol b1 b2 =
match (b1, b2) with match (b1, b2) with
| Linear (0, se1), Linear (0, se2) -> | Linear (n1, se1), Linear (n2, se2) when Z.(equal n1 zero) && Z.(equal n2 zero) ->
SymLinear.is_same_symbol se1 se2 SymLinear.is_same_symbol se1 se2
| _ -> | _ ->
None None
@ -836,5 +850,5 @@ module NonNegativeBound = struct
| None -> | None ->
Symbolic b Symbolic b
| Some c -> | Some c ->
Constant (NonNegativeInt.of_int_exn c) ) Constant (NonNegativeInt.of_big_int_exn c) )
end end

14
infer/src/bufferoverrun/bounds.mli
Unescape View File

@ -35,8 +35,8 @@ module Bound : sig
type t = type t =
| MInf | MInf
| Linear of int * SymLinear.t | Linear of Z.t * SymLinear.t
| MinMax of int * sign * min_max * int * Symb.Symbol.t | MinMax of Z.t * sign * min_max * Z.t * Symb.Symbol.t
| PInf | PInf
val compare : t -> t -> int val compare : t -> t -> int
@ -47,6 +47,8 @@ module Bound : sig
val of_int : int -> t val of_int : int -> t
val of_big_int : Z.t -> t
val minus_one : t val minus_one : t
val _255 : t val _255 : t
@ -63,11 +65,11 @@ module Bound : sig
val is_mone_symbol : t -> bool val is_mone_symbol : t -> bool
val mk_MinMax : int * sign * min_max * int * Symb.Symbol.t -> t val mk_MinMax : Z.t * sign * min_max * Z.t * Symb.Symbol.t -> t
val int_lb : t -> int sexp_option val big_int_lb : t -> Z.t sexp_option
val int_ub : t -> int sexp_option val big_int_ub : t -> Z.t sexp_option
val le : t -> t -> bool val le : t -> t -> bool
@ -97,7 +99,7 @@ module Bound : sig
val is_zero : t -> bool val is_zero : t -> bool
val is_const : t -> int sexp_option val is_const : t -> Z.t sexp_option
val plus_l : t -> t -> t val plus_l : t -> t -> t

2
infer/src/bufferoverrun/bufferOverrunDomain.ml
Unescape View File

@ -132,6 +132,8 @@ module Val = struct
let of_int n = of_itv (Itv.of_int n) let of_int n = of_itv (Itv.of_int n)
let of_big_int n = of_itv (Itv.of_big_int n)
let of_loc : Loc.t -> t = fun x -> {bot with powloc= PowLoc.singleton x} let of_loc : Loc.t -> t = fun x -> {bot with powloc= PowLoc.singleton x}
let of_pow_loc : PowLoc.t -> t = fun x -> {bot with powloc= x} let of_pow_loc : PowLoc.t -> t = fun x -> {bot with powloc= x}

12
infer/src/bufferoverrun/bufferOverrunDomainRelation.ml
Unescape View File

@ -759,11 +759,13 @@ module Make (Manager : Manager_S) = struct
let of_exp_opt ~get_sym_f opt_e : t option = Option.find_map opt_e ~f:(of_exp ~get_sym_f) let of_exp_opt ~get_sym_f opt_e : t option = Option.find_map opt_e ~f:(of_exp ~get_sym_f)
let of_int i = Texpr1.cst Env.empty (Coeff.s_of_int i) let of_big_int i =
Texpr1.cst Env.empty (Coeff.s_of_mpq (Mpq.of_mpz (Mpz.of_string (Z.to_string i))))
let zero = of_int 0
let one = of_int 1 let zero = of_big_int Z.zero
let one = of_big_int Z.one
let of_sym s = match s with Sym.V x -> Some (of_raw (Texpr1.Var x)) | _ -> None let of_sym s = match s with Sym.V x -> Some (of_raw (Texpr1.Var x)) | _ -> None
@ -897,12 +899,12 @@ module Make (Manager : Manager_S) = struct
Option.value_map (SymExp.of_sym sym) ~default:empty ~f:(fun sym_exp -> Option.value_map (SymExp.of_sym sym) ~default:empty ~f:(fun sym_exp ->
let tcons_lb = let tcons_lb =
Option.map (Itv.Bound.is_const lb) ~f:(fun lb -> Option.map (Itv.Bound.is_const lb) ~f:(fun lb ->
let sym_minus_lb = SymExp.minus sym_exp (SymExp.of_int lb) in let sym_minus_lb = SymExp.minus sym_exp (SymExp.of_big_int lb) in
Tcons1.make sym_minus_lb Tcons1.SUPEQ ) Tcons1.make sym_minus_lb Tcons1.SUPEQ )
in in
let tcons_ub = let tcons_ub =
Option.map (Itv.Bound.is_const ub) ~f:(fun ub -> Option.map (Itv.Bound.is_const ub) ~f:(fun ub ->
let ub_minus_sym = SymExp.minus (SymExp.of_int ub) sym_exp in let ub_minus_sym = SymExp.minus (SymExp.of_big_int ub) sym_exp in
Tcons1.make ub_minus_sym Tcons1.SUPEQ ) Tcons1.make ub_minus_sym Tcons1.SUPEQ )
in in
match (tcons_lb, tcons_ub) with match (tcons_lb, tcons_ub) with

2
infer/src/bufferoverrun/bufferOverrunSemantics.ml
Unescape View File

@ -15,7 +15,7 @@ open BufferOverrunDomain
let eval_const : Const.t -> Val.t = function let eval_const : Const.t -> Val.t = function
| Const.Cint intlit -> | Const.Cint intlit ->
Option.value_map ~default:Val.Itv.top ~f:Val.of_int (IntLit.to_int intlit) Val.of_big_int (IntLit.to_big_int intlit)
| Const.Cfloat f -> | Const.Cfloat f ->
f |> int_of_float |> Val.of_int f |> int_of_float |> Val.of_int
| _ -> | _ ->

69
infer/src/bufferoverrun/ints.ml
Unescape View File

@ -10,81 +10,86 @@ open! AbstractDomain.Types
module F = Format module F = Format
module NonZeroInt = struct module NonZeroInt = struct
type t = int [@@deriving compare] type t = Z.t [@@deriving compare]
exception DivisionNotExact exception DivisionNotExact
let one = 1 let one = Z.one
let minus_one = -1 let minus_one = Z.minus_one
let of_int = function 0 -> None | i -> Some i let of_big_int x = if Z.(equal x zero) then None else Some x
let opt_to_int = function None -> 0 | Some i -> i let opt_to_big_int = function None -> Z.zero | Some i -> i
let is_one = Int.equal 1 let is_one = Z.equal one
let is_minus_one = Int.equal (-1) let is_minus_one = Z.equal minus_one
let is_multiple mul div = Int.equal (mul mod div) 0 let is_multiple m d = Z.(equal (m mod d) zero)
let is_negative x = x < 0 let is_negative x = Z.(x < zero)
let is_positive x = x > 0 let is_positive x = Z.(x > zero)
let ( ~- ) = Int.( ~- ) let ( ~- ) = Z.( ~- )
let ( * ) = Int.( * ) let ( * ) = Z.( * )
let plus x y = of_int (x + y) let plus x y = of_big_int Z.(x + y)
let exact_div_exn num den = let exact_div_exn num den =
if not (is_multiple num den) then raise DivisionNotExact ; let q, r = Z.div_rem num den in
num / den if Z.(equal r zero) then q else raise DivisionNotExact
let max = Int.max let max = Z.max
let min = Int.min let min = Z.min
end end
module NonNegativeInt = struct module NonNegativeInt = struct
type t = int [@@deriving compare] type t = Z.t [@@deriving compare]
let zero = 0 let zero = Z.zero
let one = 1 let one = Z.one
let is_zero = function 0 -> true | _ -> false let is_zero = Z.equal zero
let is_one = function 1 -> true | _ -> false let is_one = Z.equal one
let of_int i = if i < 0 then None else Some i let of_big_int i = if Z.(i < zero) then None else Some i
let of_int_exn i = let of_int_exn i =
assert (i >= 0) ; assert (i >= 0) ;
Z.of_int i
let of_big_int_exn i =
assert (Z.(i >= zero)) ;
i i
let ( <= ) ~lhs ~rhs = Int.(lhs <= rhs) let ( <= ) ~lhs ~rhs = lhs <= rhs
let ( + ) = Int.( + ) let ( + ) = Z.( + )
let ( * ) = Int.( * ) let ( * ) = Z.( * )
let max = Int.max let max = Z.max
let pp = F.pp_print_int let pp = Z.pp_print
end end
module PositiveInt = struct module PositiveInt = struct
type t = NonNegativeInt.t [@@deriving compare] type t = NonNegativeInt.t [@@deriving compare]
let one = 1 let one = Z.one
let of_int i = if i <= 0 then None else Some i let of_big_int i = if Z.(i <= zero) then None else Some i
let succ = Int.succ let succ = Z.succ
let pp = F.pp_print_int let pp = Z.pp_print
end end

16
infer/src/bufferoverrun/ints.mli
Unescape View File

@ -9,7 +9,7 @@ open! IStd
module F = Format module F = Format
module NonZeroInt : sig module NonZeroInt : sig
type t = private int [@@deriving compare] type t = private Z.t [@@deriving compare]
exception DivisionNotExact exception DivisionNotExact
@ -17,15 +17,15 @@ module NonZeroInt : sig
val minus_one : t val minus_one : t
val of_int : int -> t option val of_big_int : Z.t -> t option
val opt_to_int : t option -> int val opt_to_big_int : t option -> Z.t
val is_one : t -> bool val is_one : t -> bool
val is_minus_one : t -> bool val is_minus_one : t -> bool
val is_multiple : int -> t -> bool val is_multiple : Z.t -> t -> bool
val is_negative : t -> bool val is_negative : t -> bool
@ -45,16 +45,18 @@ module NonZeroInt : sig
end end
module NonNegativeInt : sig module NonNegativeInt : sig
type t = private int [@@deriving compare] type t = private Z.t [@@deriving compare]
val zero : t val zero : t
val one : t val one : t
val of_int : int -> t option val of_big_int : Z.t -> t option
val of_int_exn : int -> t val of_int_exn : int -> t
val of_big_int_exn : Z.t -> t
val is_zero : t -> bool val is_zero : t -> bool
val is_one : t -> bool val is_one : t -> bool
@ -75,7 +77,7 @@ module PositiveInt : sig
val one : t val one : t
val of_int : int -> t option val of_big_int : Z.t -> t option
val succ : t -> t val succ : t -> t

96
infer/src/bufferoverrun/itv.ml
Unescape View File

@ -45,12 +45,12 @@ module NonNegativeBound = struct
let of_bound b = if Bound.le b zero then zero else b let of_bound b = if Bound.le b zero then zero else b
let int_lb b = let int_lb b =
Bound.int_lb b Bound.big_int_lb b
|> Option.bind ~f:NonNegativeInt.of_int |> Option.bind ~f:NonNegativeInt.of_big_int
|> Option.value ~default:NonNegativeInt.zero |> Option.value ~default:NonNegativeInt.zero
let int_ub b = Bound.int_ub b |> Option.map ~f:NonNegativeInt.of_int_exn let int_ub b = Bound.big_int_ub b |> Option.map ~f:NonNegativeInt.of_big_int_exn
let classify = function let classify = function
| Bound.PInf -> | Bound.PInf ->
@ -62,7 +62,7 @@ module NonNegativeBound = struct
| None -> | None ->
Bounds.Symbolic b Bounds.Symbolic b
| Some c -> | Some c ->
Bounds.Constant (NonNegativeInt.of_int_exn c) ) Bounds.Constant (NonNegativeInt.of_big_int_exn c) )
let subst b map = let subst b map =
@ -198,7 +198,7 @@ module MakePolynomial (S : NonNegativeSymbol) = struct
let mult_const : t -> NonNegativeInt.t -> t = let mult_const : t -> NonNegativeInt.t -> t =
fun p c -> fun p c ->
match PositiveInt.of_int (c :> int) with None -> zero | Some c -> mult_const_positive p c match PositiveInt.of_big_int (c :> Z.t) with None -> zero | Some c -> mult_const_positive p c
(* (c + r * R + s * S + t * T) x s (* (c + r * R + s * S + t * T) x s
@ -301,7 +301,7 @@ module MakePolynomial (S : NonNegativeSymbol) = struct
(fun s p acc -> (fun s p acc ->
match S.subst s eval_sym with match S.subst s eval_sym with
| Constant c -> ( | Constant c -> (
match PositiveInt.of_int (c :> int) with match PositiveInt.of_big_int (c :> Z.t) with
| None -> | None ->
acc acc
| Some c -> | Some c ->
@ -326,10 +326,10 @@ module MakePolynomial (S : NonNegativeSymbol) = struct
else ((s, PositiveInt.one), last :: others) else ((s, PositiveInt.one), last :: others)
in in
let pp_coeff fmt (c : NonNegativeInt.t) = let pp_coeff fmt (c : NonNegativeInt.t) =
if (c :> int) > 1 then F.fprintf fmt "%a * " NonNegativeInt.pp c if Z.((c :> Z.t) > one) then F.fprintf fmt "%a * " NonNegativeInt.pp c
in in
let pp_exp fmt (e : PositiveInt.t) = let pp_exp fmt (e : PositiveInt.t) =
if (e :> int) > 1 then F.fprintf fmt "^%a" PositiveInt.pp e if Z.((e :> Z.t) > one) then F.fprintf fmt "^%a" PositiveInt.pp e
in in
let pp_magic_parentheses pp fmt x = let pp_magic_parentheses pp fmt x =
let s = F.asprintf "%a" pp x in let s = F.asprintf "%a" pp x in
@ -522,6 +522,8 @@ module ItvPure = struct
let of_int n = of_bound (Bound.of_int n) let of_int n = of_bound (Bound.of_int n)
let of_big_int n = of_bound (Bound.of_big_int n)
let make_sym : unsigned:bool -> Typ.Procname.t -> SymbolTable.t -> SymbolPath.t -> Counter.t -> t let make_sym : unsigned:bool -> Typ.Procname.t -> SymbolTable.t -> SymbolPath.t -> Counter.t -> t
= =
fun ~unsigned pname symbol_table path new_sym_num -> fun ~unsigned pname symbol_table path new_sym_num ->
@ -555,10 +557,10 @@ module ItvPure = struct
let is_nat : t -> bool = function l, Bound.PInf -> Bound.is_zero l | _ -> false let is_nat : t -> bool = function l, Bound.PInf -> Bound.is_zero l | _ -> false
let is_const : t -> int option = let is_const : t -> Z.t option =
fun (l, u) -> fun (l, u) ->
match (Bound.is_const l, Bound.is_const u) with match (Bound.is_const l, Bound.is_const u) with
| Some n, Some m when Int.equal n m -> | Some n, Some m when Z.equal n m ->
Some n Some n
| _, _ -> | _, _ ->
None None
@ -593,9 +595,9 @@ module ItvPure = struct
let minus : t -> t -> t = fun i1 i2 -> plus i1 (neg i2) let minus : t -> t -> t = fun i1 i2 -> plus i1 (neg i2)
let mult_const : int -> t -> t = let mult_const : Z.t -> t -> t =
fun n ((l, u) as itv) -> fun n ((l, u) as itv) ->
match NonZeroInt.of_int n with match NonZeroInt.of_big_int n with
| None -> | None ->
zero zero
| Some n -> | Some n ->
@ -607,9 +609,9 @@ module ItvPure = struct
(* Returns a precise value only when all coefficients are divided by (* Returns a precise value only when all coefficients are divided by
n without remainder. *) n without remainder. *)
let div_const : t -> int -> t = let div_const : t -> Z.t -> t =
fun ((l, u) as itv) n -> fun ((l, u) as itv) n ->
match NonZeroInt.of_int n with match NonZeroInt.of_big_int n with
| None -> | None ->
top top
| Some n -> | Some n ->
@ -643,34 +645,40 @@ module ItvPure = struct
match is_const y with match is_const y with
| None -> | None ->
top top
| Some 0 -> | Some n when Z.(equal n zero) ->
x (* x % [0,0] does nothing. *) x (* x % [0,0] does nothing. *)
| Some m -> ( | Some m -> (
match is_const x with match is_const x with
| Some n -> | Some n ->
of_int (n mod m) of_big_int Z.(n mod m)
| None -> | None ->
let abs_m = abs m in let abs_m = Z.abs m in
if is_ge_zero x then (Bound.zero, Bound.of_int (abs_m - 1)) if is_ge_zero x then (Bound.zero, Bound.of_big_int Z.(abs_m - one))
else if is_le_zero x then (Bound.of_int (-abs_m + 1), Bound.zero) else if is_le_zero x then (Bound.of_big_int Z.(one - abs_m), Bound.zero)
else (Bound.of_int (-abs_m + 1), Bound.of_int (abs_m - 1)) ) else (Bound.of_big_int Z.(one - abs_m), Bound.of_big_int Z.(abs_m - one)) )
(* x << [-1,-1] does nothing. *) (* x << [-1,-1] does nothing. *)
let shiftlt : t -> t -> t = let shiftlt : t -> t -> t =
fun x y -> match is_const y with Some n -> mult_const (1 lsl n) x | None -> top fun x y ->
Option.value_map (is_const y) ~default:top ~f:(fun n ->
match Z.to_int n with
| n ->
if n < 0 then x else mult_const Z.(one lsl n) x
| exception Z.Overflow ->
top )
(* x >> [-1,-1] does nothing. *) (* x >> [-1,-1] does nothing. *)
let shiftrt : t -> t -> t = let shiftrt : t -> t -> t =
fun x y -> fun x y ->
match is_const y with match is_const y with
| Some n when Int.( <= ) n 0 -> | Some n when Z.(leq n zero) ->
x x
| Some n when n >= 64 -> | Some n when Z.(n >= of_int 64) ->
zero zero
| Some n -> | Some n -> (
div_const x (1 lsl n) match Z.to_int n with n -> div_const x Z.(one lsl n) | exception Z.Overflow -> top )
| None -> | None ->
top top
@ -734,27 +742,27 @@ module ItvPure = struct
| (l1, Bound.PInf), (_, u2) -> | (l1, Bound.PInf), (_, u2) ->
(l1, u2) (l1, u2)
| (l1, Bound.Linear (c1, s1)), (_, Bound.Linear (c2, s2)) when Bounds.SymLinear.eq s1 s2 -> | (l1, Bound.Linear (c1, s1)), (_, Bound.Linear (c2, s2)) when Bounds.SymLinear.eq s1 s2 ->
(l1, Bound.Linear (min c1 c2, s1)) (l1, Bound.Linear (Z.(min c1 c2), s1))
| (l1, Bound.Linear (c, se)), (_, u) when Bounds.SymLinear.is_zero se && Bound.is_one_symbol u | (l1, Bound.Linear (c, se)), (_, u) when Bounds.SymLinear.is_zero se && Bound.is_one_symbol u
-> ->
(l1, Bound.mk_MinMax (0, Bound.Plus, Bound.Min, c, Bound.get_one_symbol u)) (l1, Bound.mk_MinMax (Z.zero, Bound.Plus, Bound.Min, c, Bound.get_one_symbol u))
| (l1, u), (_, Bound.Linear (c, se)) when Bounds.SymLinear.is_zero se && Bound.is_one_symbol u | (l1, u), (_, Bound.Linear (c, se)) when Bounds.SymLinear.is_zero se && Bound.is_one_symbol u
-> ->
(l1, Bound.mk_MinMax (0, Bound.Plus, Bound.Min, c, Bound.get_one_symbol u)) (l1, Bound.mk_MinMax (Z.zero, Bound.Plus, Bound.Min, c, Bound.get_one_symbol u))
| (l1, Bound.Linear (c, se)), (_, u) when Bounds.SymLinear.is_zero se && Bound.is_mone_symbol u | (l1, Bound.Linear (c, se)), (_, u) when Bounds.SymLinear.is_zero se && Bound.is_mone_symbol u
-> ->
(l1, Bound.mk_MinMax (0, Bound.Minus, Bound.Max, -c, Bound.get_mone_symbol u)) (l1, Bound.mk_MinMax (Z.zero, Bound.Minus, Bound.Max, Z.neg c, Bound.get_mone_symbol u))
| (l1, u), (_, Bound.Linear (c, se)) when Bounds.SymLinear.is_zero se && Bound.is_mone_symbol u | (l1, u), (_, Bound.Linear (c, se)) when Bounds.SymLinear.is_zero se && Bound.is_mone_symbol u
-> ->
(l1, Bound.mk_MinMax (0, Bound.Minus, Bound.Max, -c, Bound.get_mone_symbol u)) (l1, Bound.mk_MinMax (Z.zero, Bound.Minus, Bound.Max, Z.neg c, Bound.get_mone_symbol u))
| (l1, Bound.Linear (c1, se)), (_, Bound.MinMax (c2, Bound.Plus, Bound.Min, d2, se')) | (l1, Bound.Linear (c1, se)), (_, Bound.MinMax (c2, Bound.Plus, Bound.Min, d2, se'))
| (l1, Bound.MinMax (c2, Bound.Plus, Bound.Min, d2, se')), (_, Bound.Linear (c1, se)) | (l1, Bound.MinMax (c2, Bound.Plus, Bound.Min, d2, se')), (_, Bound.Linear (c1, se))
when Bounds.SymLinear.is_zero se -> when Bounds.SymLinear.is_zero se ->
(l1, Bound.mk_MinMax (c2, Bound.Plus, Bound.Min, min (c1 - c2) d2, se')) (l1, Bound.mk_MinMax (c2, Bound.Plus, Bound.Min, Z.(min (c1 - c2) d2), se'))
| ( (l1, Bound.MinMax (c1, Bound.Plus, Bound.Min, d1, se1)) | ( (l1, Bound.MinMax (c1, Bound.Plus, Bound.Min, d1, se1))
, (_, Bound.MinMax (c2, Bound.Plus, Bound.Min, d2, se2)) ) , (_, Bound.MinMax (c2, Bound.Plus, Bound.Min, d2, se2)) )
when Int.equal c1 c2 && Symbol.equal se1 se2 -> when Z.equal c1 c2 && Symbol.equal se1 se2 ->
(l1, Bound.mk_MinMax (c1, Bound.Plus, Bound.Min, min d1 d2, se1)) (l1, Bound.mk_MinMax (c1, Bound.Plus, Bound.Min, Z.min d1 d2, se1))
| _ -> | _ ->
x x
@ -765,27 +773,27 @@ module ItvPure = struct
| (Bound.MInf, u1), (l2, _) -> | (Bound.MInf, u1), (l2, _) ->
(l2, u1) (l2, u1)
| (Bound.Linear (c1, s1), u1), (Bound.Linear (c2, s2), _) when Bounds.SymLinear.eq s1 s2 -> | (Bound.Linear (c1, s1), u1), (Bound.Linear (c2, s2), _) when Bounds.SymLinear.eq s1 s2 ->
(Bound.Linear (max c1 c2, s1), u1) (Bound.Linear (Z.max c1 c2, s1), u1)
| (Bound.Linear (c, se), u1), (l, _) when Bounds.SymLinear.is_zero se && Bound.is_one_symbol l | (Bound.Linear (c, se), u1), (l, _) when Bounds.SymLinear.is_zero se && Bound.is_one_symbol l
-> ->
(Bound.mk_MinMax (0, Bound.Plus, Bound.Max, c, Bound.get_one_symbol l), u1) (Bound.mk_MinMax (Z.zero, Bound.Plus, Bound.Max, c, Bound.get_one_symbol l), u1)
| (l, u1), (Bound.Linear (c, se), _) when Bounds.SymLinear.is_zero se && Bound.is_one_symbol l | (l, u1), (Bound.Linear (c, se), _) when Bounds.SymLinear.is_zero se && Bound.is_one_symbol l
-> ->
(Bound.mk_MinMax (0, Bound.Plus, Bound.Max, c, Bound.get_one_symbol l), u1) (Bound.mk_MinMax (Z.zero, Bound.Plus, Bound.Max, c, Bound.get_one_symbol l), u1)
| (Bound.Linear (c, se), u1), (l, _) when Bounds.SymLinear.is_zero se && Bound.is_mone_symbol l | (Bound.Linear (c, se), u1), (l, _) when Bounds.SymLinear.is_zero se && Bound.is_mone_symbol l
-> ->
(Bound.mk_MinMax (0, Bound.Minus, Bound.Min, c, Bound.get_mone_symbol l), u1) (Bound.mk_MinMax (Z.zero, Bound.Minus, Bound.Min, c, Bound.get_mone_symbol l), u1)
| (l, u1), (Bound.Linear (c, se), _) when Bounds.SymLinear.is_zero se && Bound.is_mone_symbol l | (l, u1), (Bound.Linear (c, se), _) when Bounds.SymLinear.is_zero se && Bound.is_mone_symbol l
-> ->
(Bound.mk_MinMax (0, Bound.Minus, Bound.Min, c, Bound.get_mone_symbol l), u1) (Bound.mk_MinMax (Z.zero, Bound.Minus, Bound.Min, c, Bound.get_mone_symbol l), u1)
| (Bound.Linear (c1, se), u1), (Bound.MinMax (c2, Bound.Plus, Bound.Max, d2, se'), _) | (Bound.Linear (c1, se), u1), (Bound.MinMax (c2, Bound.Plus, Bound.Max, d2, se'), _)
| (Bound.MinMax (c2, Bound.Plus, Bound.Max, d2, se'), u1), (Bound.Linear (c1, se), _) | (Bound.MinMax (c2, Bound.Plus, Bound.Max, d2, se'), u1), (Bound.Linear (c1, se), _)
when Bounds.SymLinear.is_zero se -> when Bounds.SymLinear.is_zero se ->
(Bound.mk_MinMax (c2, Bound.Plus, Bound.Max, max (c1 - c2) d2, se'), u1) (Bound.mk_MinMax (c2, Bound.Plus, Bound.Max, Z.(max (c1 - c2) d2), se'), u1)
| ( (Bound.MinMax (c1, Bound.Plus, Bound.Max, d1, se1), u1) | ( (Bound.MinMax (c1, Bound.Plus, Bound.Max, d1, se1), u1)
, (Bound.MinMax (c2, Bound.Plus, Bound.Max, d2, se2), _) ) , (Bound.MinMax (c2, Bound.Plus, Bound.Max, d2, se2), _) )
when Int.equal c1 c2 && Symbol.equal se1 se2 -> when Z.equal c1 c2 && Symbol.equal se1 se2 ->
(Bound.mk_MinMax (c1, Bound.Plus, Bound.Max, max d1 d2, se1), u1) (Bound.mk_MinMax (c1, Bound.Plus, Bound.Max, Z.max d1 d2, se1), u1)
| _ -> | _ ->
x x
@ -915,11 +923,11 @@ let of_bool = function
let of_int : int -> astate = fun n -> NonBottom (ItvPure.of_int n) let of_int : int -> astate = fun n -> NonBottom (ItvPure.of_int n)
let of_int_lit n = Option.value_map ~default:top ~f:of_int (IntLit.to_int n) let of_big_int : Z.t -> astate = fun n -> NonBottom (ItvPure.of_big_int n)
let of_int64 : Int64.t -> astate = let of_int_lit : IntLit.t -> astate = fun n -> of_big_int (IntLit.to_big_int n)
fun n -> Int64.to_int n |> Option.value_map ~f:of_int ~default:top
let of_int64 : Int64.t -> astate = fun n -> of_big_int (Z.of_int64 n)
let is_false : t -> bool = function NonBottom x -> ItvPure.is_false x | Bottom -> false let is_false : t -> bool = function NonBottom x -> ItvPure.is_false x | Bottom -> false

2
infer/src/bufferoverrun/itv.mli
Unescape View File

@ -160,6 +160,8 @@ val of_bool : Boolean.t -> t
val of_int : int -> t val of_int : int -> t
val of_big_int : Z.t -> t
val of_int_lit : IntLit.t -> t val of_int_lit : IntLit.t -> t
val of_int64 : Int64.t -> t val of_int64 : Int64.t -> t

1
infer/src/dune.common.in
Unescape View File

@ -71,4 +71,5 @@ let common_libraries =
; "unix" ; "unix"
; "xmlm" ; "xmlm"
; "yojson" ; "yojson"
; "zarith"
; "zip" ] ; "zip" ]

28
infer/tests/codetoanalyze/c/bufferoverrun/arith.c
Unescape View File

@ -140,3 +140,31 @@ void integer_overflow_by_multiplication_Bad_FN() {
arr[z] = 0; arr[z] = 0;
} }
} }
void use_int64_max_Good() {
char arr[10];
int64_t x = INT64_MAX;
int64_t y = INT64_MAX - 5;
arr[x - y] = 0;
}
void use_int64_max_Bad() {
char arr[10];
int64_t x = INT64_MAX;
int64_t y = INT64_MAX - 15;
arr[x - y] = 0;
}
void use_uint64_max_Good() {
char arr[10];
uint64_t x = UINT64_MAX;
uint64_t y = UINT64_MAX - 5;
arr[x - y] = 0;
}
void use_uint64_max_Bad_FN() {
char arr[10];
uint64_t x = UINT64_MAX;
uint64_t y = UINT64_MAX - 15;
arr[x - y] = 0;
}

1
infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
Unescape View File

@ -6,6 +6,7 @@ codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_neg_Bad, 2, BUFFER_OVERRUN_
codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min2_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 14] Size: 10] codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min2_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 14] Size: 10]
codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min3_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 25] Size: 20] codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min3_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 25] Size: 20]
codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 19] Size: 19] codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 19] Size: 19]
codetoanalyze/c/bufferoverrun/arith.c, use_int64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 15 Size: 10]
codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Offset: [3xlen.lb + 1, 3xlen.ub + 1] Size: [3xlen.lb + 1, 3xlen.ub + 1]] codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Offset: [3xlen.lb + 1, 3xlen.ub + 1] Size: [3xlen.lb + 1, 3xlen.ub + 1]]
codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 20 Size: 10] codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 20 Size: 10]
codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Assignment,Assignment,ArrayAccess: Offset: -1 Size: 2] codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Assignment,Assignment,ArrayAccess: Offset: -1 Size: 2]

1
opam
Unescape View File

@ -50,6 +50,7 @@ depends: [
"sawja" {>="1.5.4"} "sawja" {>="1.5.4"}
"sqlite3" "sqlite3"
"xmlm" {>="1.2.0"} "xmlm" {>="1.2.0"}
"zarith" {>="1.7"}
] ]
depexts: [ depexts: [
[ ["ubuntu"] ["python2.7-dev"] ] [ ["ubuntu"] ["python2.7-dev"] ]

1
opam.lock
Unescape View File

@ -92,3 +92,4 @@ typerep = v0.11.0
variantslib = v0.11.0 variantslib = v0.11.0
xmlm = 1.3.0 xmlm = 1.3.0
yojson = 1.4.1 yojson = 1.4.1
zarith = 1.7

Write Preview
Loading…
Cancel
Save