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

[inferbo] More physical equalities for Bounds

Browse Source 
Reviewed By: skcho

Differential Revision: D13176079

fbshipit-source-id: e09ebd176
master
Mehdi Bouaziz 6 years ago committed by Facebook Github Bot
parent 03d3a85f45
commit bdbf39aaa3
1 changed files with 175 additions and 162 deletions
Show Stats Download Patch File Download Diff File

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

@ -41,6 +41,8 @@ module SymLinear = struct
let le : t -> t -> bool = let le : t -> t -> bool =
fun x y -> fun x y ->
phys_equal 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_big_int v1_opt in let v1 = NonZeroInt.opt_to_big_int v1_opt in
let v2 = NonZeroInt.opt_to_big_int v2_opt in let v2 = NonZeroInt.opt_to_big_int v2_opt in
@ -82,13 +84,15 @@ module SymLinear = struct
let plus : t -> t -> t = let plus : t -> t -> t =
fun x y -> fun x y ->
let plus_coeff _ c1 c2 = NonZeroInt.plus c1 c2 in let plus_coeff _ c1 c2 = NonZeroInt.plus c1 c2 in
M.union plus_coeff x y PhysEqual.optim2 x y ~res:(M.union plus_coeff x y)
let mult_const : NonZeroInt.t -> t -> t = fun n x -> M.map (NonZeroInt.( * ) n) x let mult_const : NonZeroInt.t -> t -> t =
fun n x -> if NonZeroInt.is_one n then x else M.map (NonZeroInt.( * ) n) x
let exact_div_const_exn : t -> NonZeroInt.t -> t = let exact_div_const_exn : t -> NonZeroInt.t -> t =
fun x n -> M.map (fun c -> NonZeroInt.exact_div_exn c n) x fun x n -> if NonZeroInt.is_one n then x else M.map (fun c -> NonZeroInt.exact_div_exn c n) x
(* Returns a symbol when the map contains only one symbol s with a (* Returns a symbol when the map contains only one symbol s with a
@ -445,8 +449,8 @@ module Bound = struct
PInf PInf
| PInf -> | PInf ->
MInf MInf
| Linear (c, x) -> | Linear (c, x) as b ->
Linear (Z.neg c, SymLinear.neg x) if Z.(equal c zero) && SymLinear.is_zero x then b else Linear (Z.neg c, SymLinear.neg x)
| MinMax (c, sign, min_max, d, x) -> | MinMax (c, sign, min_max, d, x) ->
mk_MinMax (Z.neg c, Sign.neg sign, min_max, d, x) mk_MinMax (Z.neg c, Sign.neg sign, min_max, d, x)
@ -619,9 +623,15 @@ module Bound = struct
overapprox_min original_b1 b2 overapprox_min original_b1 b2
let underapprox_max b1 b2 = neg (overapprox_min (neg b1) (neg b2)) let underapprox_max b1 b2 =
let res = neg (overapprox_min (neg b1) (neg b2)) in
if equal res b1 then b1 else if equal res b2 then b2 else res
let overapprox_max b1 b2 =
let res = neg (underapprox_min (neg b1) (neg b2)) in
if equal res b1 then b1 else if equal res b2 then b2 else res
let overapprox_max b1 b2 = neg (underapprox_min (neg b1) (neg b2))
let approx_max = function let approx_max = function
| Symb.BoundEnd.LowerBound -> | Symb.BoundEnd.LowerBound ->
@ -678,19 +688,18 @@ module Bound = struct
let plus_common : f:(t -> t -> t) -> t -> t -> t = let plus_common : f:(t -> t -> t) -> t -> t -> t =
fun ~f x y -> fun ~f x y ->
match (x, y) with if is_zero x then y
| _, _ when is_zero x -> else if is_zero y then x
y else
| _, _ when is_zero y -> match (x, y) with
x | Linear (c1, x1), Linear (c2, x2) ->
| Linear (c1, x1), Linear (c2, x2) -> Linear (Z.(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 (Z.(c1 + c2), sign, min_max, d1, x1)
mk_MinMax (Z.(c1 + c2), sign, min_max, d1, x1) | _ ->
| _ -> f x y
f x y
let plus_l : t -> t -> t = let plus_l : t -> t -> t =
@ -723,25 +732,27 @@ module Bound = struct
let mult_const : Symb.BoundEnd.t -> NonZeroInt.t -> t -> t = let mult_const : Symb.BoundEnd.t -> NonZeroInt.t -> t -> t =
fun bound_end n x -> fun bound_end n x ->
match x with if NonZeroInt.is_one n then x
| MInf -> else
if NonZeroInt.is_positive n then MInf else PInf match x with
| PInf -> | MInf ->
if NonZeroInt.is_positive n then PInf else MInf if NonZeroInt.is_positive n then MInf else PInf
| Linear (c, x') -> | PInf ->
Linear (Z.(c * (n :> Z.t)), SymLinear.mult_const n x') if NonZeroInt.is_positive n then PInf else MInf
| MinMax _ -> ( | Linear (c, x') ->
let int_bound = Linear (Z.(c * (n :> Z.t)), SymLinear.mult_const n x')
let bound_end' = | MinMax _ -> (
if NonZeroInt.is_positive n then bound_end else Symb.BoundEnd.neg bound_end let int_bound =
let bound_end' =
if NonZeroInt.is_positive n then bound_end else Symb.BoundEnd.neg bound_end
in
big_int_of_minmax bound_end' x
in in
big_int_of_minmax bound_end' x match int_bound with
in | Some i ->
match int_bound with of_big_int Z.(i * (n :> Z.t))
| Some i -> | None ->
of_big_int Z.(i * (n :> Z.t)) of_bound_end bound_end )
| None ->
of_bound_end bound_end )
let mult_const_l = mult_const Symb.BoundEnd.LowerBound let mult_const_l = mult_const Symb.BoundEnd.LowerBound
@ -760,30 +771,32 @@ module Bound = struct
let div_const : Symb.BoundEnd.t -> t -> NonZeroInt.t -> t option = let div_const : Symb.BoundEnd.t -> t -> NonZeroInt.t -> t option =
fun bound_end x n -> fun bound_end x n ->
match x with if NonZeroInt.is_one n then Some x
| MInf -> else
Some (if NonZeroInt.is_positive n then MInf else PInf) match x with
| PInf -> | MInf ->
Some (if NonZeroInt.is_positive n then PInf else MInf) Some (if NonZeroInt.is_positive n then MInf else PInf)
| Linear (c, x') when SymLinear.is_zero x' -> | PInf ->
Some (Linear (Z.(c / (n :> Z.t)), SymLinear.zero)) Some (if NonZeroInt.is_positive n then PInf else MInf)
| Linear (c, x') when NonZeroInt.is_multiple c n -> ( | Linear (c, x') when SymLinear.is_zero x' ->
match SymLinear.exact_div_const_exn x' n with Some (Linear (Z.(c / (n :> Z.t)), SymLinear.zero))
| x'' -> | Linear (c, x') when NonZeroInt.is_multiple c n -> (
Some (Linear (Z.(c / (n :> Z.t)), x'')) match SymLinear.exact_div_const_exn x' n with
| exception NonZeroInt.DivisionNotExact -> | x'' ->
None ) Some (Linear (Z.(c / (n :> Z.t)), x''))
| MinMax _ -> | exception NonZeroInt.DivisionNotExact ->
let c = None )
match bound_end with | MinMax _ ->
| Symb.BoundEnd.LowerBound -> let c =
underapprox_minmax_div_const x n match bound_end with
| Symb.BoundEnd.UpperBound -> | Symb.BoundEnd.LowerBound ->
overapprox_minmax_div_const x n underapprox_minmax_div_const x n
in | Symb.BoundEnd.UpperBound ->
Option.map c ~f:of_big_int overapprox_minmax_div_const x n
| _ -> in
None Option.map c ~f:of_big_int
| _ ->
None
let div_const_l = div_const Symb.BoundEnd.LowerBound let div_const_l = div_const Symb.BoundEnd.LowerBound
@ -803,110 +816,110 @@ module Bound = struct
let is_not_infty : t -> bool = function MInf | PInf -> false | _ -> true let is_not_infty : t -> bool = function MInf | PInf -> false | _ -> true
let lift1 : (t -> t) -> t bottom_lifted -> t bottom_lifted =
fun f x -> match x with Bottom -> Bottom | NonBottom x -> NonBottom (f x)
let lift2 : (t -> t -> t) -> t bottom_lifted -> t bottom_lifted -> t bottom_lifted =
fun f x y ->
match (x, y) with
| Bottom, _ | _, Bottom ->
Bottom
| NonBottom x, NonBottom y ->
NonBottom (f x y)
(** Substitutes ALL symbols in [x] with respect to [eval_sym]. Under/over-Approximate as good as possible according to [subst_pos]. *) (** Substitutes ALL symbols in [x] with respect to [eval_sym]. Under/over-Approximate as good as possible according to [subst_pos]. *)
let subst : subst_pos:Symb.BoundEnd.t -> t -> eval_sym -> t bottom_lifted = let subst : subst_pos:Symb.BoundEnd.t -> t -> eval_sym -> t bottom_lifted =
fun ~subst_pos x eval_sym -> let lift1 : (t -> t) -> t bottom_lifted -> t bottom_lifted =
let get s = fun f x -> match x with Bottom -> Bottom | NonBottom x -> NonBottom (f x)
match eval_sym s with
| NonBottom x when Symb.Symbol.is_unsigned s ->
NonBottom (approx_max subst_pos x zero)
| x ->
x
in in
let get_mult_const s coeff = let lift2 : (t -> t -> t) -> t bottom_lifted -> t bottom_lifted -> t bottom_lifted =
if NonZeroInt.is_one coeff then get s fun f x y ->
else if NonZeroInt.is_minus_one coeff then get s |> lift1 neg match (x, y) with
else | Bottom, _ | _, Bottom ->
match eval_sym s with Bottom
| Bottom -> ( | NonBottom x, NonBottom y ->
(* For unsigned symbols, we can over/under-approximate with zero depending on [subst_pos] and the sign of the coefficient. *) NonBottom (f x y)
match (Symb.Symbol.is_unsigned s, subst_pos, NonZeroInt.is_positive coeff) with
| true, Symb.BoundEnd.LowerBound, true | true, Symb.BoundEnd.UpperBound, false ->
NonBottom zero
| _ ->
Bottom )
| NonBottom x ->
let x = mult_const subst_pos coeff x in
if Symb.Symbol.is_unsigned s then NonBottom (approx_max subst_pos x zero)
else NonBottom x
in in
match x with fun ~subst_pos x eval_sym ->
| MInf | PInf -> let get s =
NonBottom x match eval_sym s with
| Linear (c, se) -> | NonBottom x when Symb.Symbol.is_unsigned s ->
SymLinear.fold se NonBottom (approx_max subst_pos x zero)
~init:(NonBottom (of_big_int c)) | x ->
~f:(fun acc s coeff -> lift2 (plus subst_pos) acc (get_mult_const s coeff)) x
| MinMax (c, sign, min_max, d, s) -> ( in
match get s with let get_mult_const s coeff =
| Bottom -> if NonZeroInt.is_one coeff then get s
Option.value_map (big_int_of_minmax subst_pos x) ~default:Bottom ~f:(fun i -> else if NonZeroInt.is_minus_one coeff then get s |> lift1 neg
NonBottom (of_big_int i) ) else
| NonBottom x' -> match eval_sym s with
let res = | Bottom -> (
match (sign, min_max, x') with (* For unsigned symbols, we can over/under-approximate with zero depending on [subst_pos] and the sign of the coefficient. *)
| Plus, Min, MInf | Minus, Max, PInf -> match (Symb.Symbol.is_unsigned s, subst_pos, NonZeroInt.is_positive coeff) with
MInf | true, Symb.BoundEnd.LowerBound, true | true, Symb.BoundEnd.UpperBound, false ->
| Plus, Max, PInf | Minus, Min, MInf -> NonBottom zero
PInf | _ ->
| sign, Min, PInf | sign, Max, MInf -> Bottom )
of_big_int (Sign.eval_big_int sign c d) | NonBottom x ->
| _, _, Linear (c2, se) -> ( let x = mult_const subst_pos coeff x in
if SymLinear.is_zero se then if Symb.Symbol.is_unsigned s then NonBottom (approx_max subst_pos x zero)
of_big_int (Sign.eval_big_int sign c (MinMax.eval_big_int min_max d c2)) else NonBottom x
else if SymLinear.is_one_symbol se then in
mk_MinMax match x with
( Sign.eval_big_int sign c c2 | MInf | PInf ->
, sign NonBottom x
, min_max | Linear (c, se) ->
, Z.(d - c2) if SymLinear.is_empty se then NonBottom x
, SymLinear.get_one_symbol se ) else
else if SymLinear.is_mone_symbol se then SymLinear.fold se
mk_MinMax ~init:(NonBottom (of_big_int c))
( Sign.eval_big_int sign c c2 ~f:(fun acc s coeff -> lift2 (plus subst_pos) acc (get_mult_const s coeff))
, Sign.neg sign | MinMax (c, sign, min_max, d, s) -> (
, MinMax.neg min_max match get s with
, Z.(c2 - d) | Bottom ->
, SymLinear.get_mone_symbol se ) Option.value_map (big_int_of_minmax subst_pos x) ~default:Bottom ~f:(fun i ->
else NonBottom (of_big_int i) )
match big_int_of_minmax subst_pos x with | NonBottom x' ->
| Some i -> let res =
of_big_int i match (sign, min_max, x') with
| None -> | Plus, Min, MInf | Minus, Max, PInf ->
of_bound_end subst_pos ) MInf
| _, _, MinMax (c2, sign2, min_max2, d2, s2) -> ( | Plus, Max, PInf | Minus, Min, MInf ->
match (min_max, sign2, min_max2) with PInf
| Min, Plus, Min | Max, Plus, Max -> | sign, Min, PInf | sign, Max, MInf ->
let c' = Sign.eval_big_int sign c c2 in of_big_int (Sign.eval_big_int sign c d)
let d' = MinMax.eval_big_int min_max Z.(d - c2) d2 in | _, _, Linear (c2, se) -> (
mk_MinMax (c', sign, min_max, d', s2) if SymLinear.is_zero se then
| Min, Minus, Max | Max, Minus, Min -> of_big_int (Sign.eval_big_int sign c (MinMax.eval_big_int min_max d c2))
let c' = Sign.eval_big_int sign c c2 in else if SymLinear.is_one_symbol se then
let d' = MinMax.eval_big_int min_max2 Z.(c2 - d) d2 in mk_MinMax
mk_MinMax (c', Sign.neg sign, min_max2, d', s2) ( Sign.eval_big_int sign c c2
| _ -> , sign
let bound_end = , min_max
match sign with Plus -> subst_pos | Minus -> Symb.BoundEnd.neg subst_pos , Z.(d - c2)
in , SymLinear.get_one_symbol se )
of_big_int else if SymLinear.is_mone_symbol se then
(Sign.eval_big_int sign c mk_MinMax
(MinMax.eval_big_int min_max d ( Sign.eval_big_int sign c c2
(big_int_of_minmax bound_end x' |> Option.value ~default:d))) ) , Sign.neg sign
in , MinMax.neg min_max
NonBottom res ) , Z.(c2 - d)
, SymLinear.get_mone_symbol se )
else
match big_int_of_minmax subst_pos x with
| Some i ->
of_big_int i
| None ->
of_bound_end subst_pos )
| _, _, MinMax (c2, sign2, min_max2, d2, s2) -> (
match (min_max, sign2, min_max2) with
| Min, Plus, Min | Max, Plus, Max ->
let c' = Sign.eval_big_int sign c c2 in
let d' = MinMax.eval_big_int min_max Z.(d - c2) d2 in
mk_MinMax (c', sign, min_max, d', s2)
| Min, Minus, Max | Max, Minus, Min ->
let c' = Sign.eval_big_int sign c c2 in
let d' = MinMax.eval_big_int min_max2 Z.(c2 - d) d2 in
mk_MinMax (c', Sign.neg sign, min_max2, d', s2)
| _ ->
let bound_end =
match sign with Plus -> subst_pos | Minus -> Symb.BoundEnd.neg subst_pos
in
of_big_int
(Sign.eval_big_int sign c
(MinMax.eval_big_int min_max d
(big_int_of_minmax bound_end x' |> Option.value ~default:d))) )
in
NonBottom res )
let subst_lb x eval_sym = subst ~subst_pos:Symb.BoundEnd.LowerBound x eval_sym let subst_lb x eval_sym = subst ~subst_pos:Symb.BoundEnd.LowerBound x eval_sym

Write Preview
Loading…
Cancel
Save