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

[inferbo] Comparisons return abstract boolean

Browse Source 
Summary:
Got rid of `Itv.equal` which was ambiguous and use an abstract boolean type for abstract comparison results
Depends on D7568573

Reviewed By: jvillard

Differential Revision: D7568583

fbshipit-source-id: 0e897e9
master
Mehdi Bouaziz 7 years ago committed by Facebook Github Bot
parent 9eeeecc338
commit 5925c75e29
4 changed files with 136 additions and 100 deletions
Show Stats Download Patch File Download Diff File

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

@ -113,7 +113,7 @@ module Val = struct
let neg : t -> t = fun x -> {x with itv= Itv.neg x.itv} let neg : t -> t = fun x -> {x with itv= Itv.neg x.itv}
let lnot : t -> t = fun x -> {x with itv= Itv.lnot x.itv} let lnot : t -> t = fun x -> {x with itv= Itv.lnot x.itv |> Itv.of_bool}
let lift_itv : (Itv.t -> Itv.t -> Itv.t) -> t -> t -> t = let lift_itv : (Itv.t -> Itv.t -> Itv.t) -> t -> t -> t =
fun f x y -> {bot with itv= f x.itv y.itv; traces= TraceSet.join x.traces y.traces} fun f x y -> {bot with itv= f x.itv y.itv; traces= TraceSet.join x.traces y.traces}
@ -121,11 +121,11 @@ module Val = struct
let has_pointer : t -> bool = fun x -> not (PowLoc.is_bot x.powloc && ArrayBlk.is_bot x.arrayblk) let has_pointer : t -> bool = fun x -> not (PowLoc.is_bot x.powloc && ArrayBlk.is_bot x.arrayblk)
let lift_cmp_itv : (Itv.t -> Itv.t -> Itv.t) -> t -> t -> t = let lift_cmp_itv : (Itv.t -> Itv.t -> Itv.Boolean.t) -> t -> t -> t =
fun f x y -> fun f x y ->
if has_pointer x || has_pointer y then let b = if has_pointer x || has_pointer y then Itv.Boolean.top else f x.itv y.itv in
{bot with itv= Itv.unknown_bool; traces= TraceSet.join x.traces y.traces} let itv = Itv.of_bool b in
else lift_itv f x y {bot with itv; traces= TraceSet.join x.traces y.traces}
let plus_a : t -> t -> t = lift_itv Itv.plus let plus_a : t -> t -> t = lift_itv Itv.plus
@ -154,9 +154,9 @@ module Val = struct
let ne_sem : t -> t -> t = lift_cmp_itv Itv.ne_sem let ne_sem : t -> t -> t = lift_cmp_itv Itv.ne_sem
let land_sem : t -> t -> t = lift_itv Itv.land_sem let land_sem : t -> t -> t = lift_cmp_itv Itv.land_sem
let lor_sem : t -> t -> t = lift_itv Itv.lor_sem let lor_sem : t -> t -> t = lift_cmp_itv Itv.lor_sem
let lift_prune1 : (Itv.t -> Itv.t) -> t -> t = fun f x -> {x with itv= f x.itv} let lift_prune1 : (Itv.t -> Itv.t) -> t -> t = fun f x -> {x with itv= f x.itv}

16
infer/src/bufferoverrun/bufferOverrunProofObligations.ml
Unescape View File

@ -43,14 +43,14 @@ module AllocSizeCondition = struct
| (`LeftSmallerThanRight | `RightSmallerThanLeft) as cmp -> | (`LeftSmallerThanRight | `RightSmallerThanLeft) as cmp ->
let lpos = ItvPure.le_sem ItvPure.zero lhs in let lpos = ItvPure.le_sem ItvPure.zero lhs in
let rpos = ItvPure.le_sem ItvPure.zero rhs in let rpos = ItvPure.le_sem ItvPure.zero rhs in
if not (ItvPure.equal lpos rpos) then `NotComparable if not (Itv.Boolean.equal lpos rpos) then `NotComparable
else if ItvPure.is_true lpos then else if Itv.Boolean.is_true lpos then
match cmp with match cmp with
| `LeftSmallerThanRight -> | `LeftSmallerThanRight ->
`RightSubsumesLeft `RightSubsumesLeft
| `RightSmallerThanLeft -> | `RightSmallerThanLeft ->
`LeftSubsumesRight `LeftSubsumesRight
else if ItvPure.is_false lpos then else if Itv.Boolean.is_false lpos then
match cmp with match cmp with
| `LeftSmallerThanRight -> | `LeftSmallerThanRight ->
`LeftSubsumesRight `LeftSubsumesRight
@ -147,8 +147,8 @@ module ArrayAccessCondition = struct
| (`LeftSmallerThanRight | `RightSmallerThanLeft), _ -> | (`LeftSmallerThanRight | `RightSmallerThanLeft), _ ->
let lidxpos = ItvPure.le_sem ItvPure.zero lidx in let lidxpos = ItvPure.le_sem ItvPure.zero lidx in
let ridxpos = ItvPure.le_sem ItvPure.zero ridx in let ridxpos = ItvPure.le_sem ItvPure.zero ridx in
if not (ItvPure.equal lidxpos ridxpos) then `NotComparable if not (Itv.Boolean.equal lidxpos ridxpos) then `NotComparable
else if ItvPure.is_true lidxpos then else if Itv.Boolean.is_true lidxpos then
(* both idx >= 0 *) (* both idx >= 0 *)
match (idxcmp, sizcmp) with match (idxcmp, sizcmp) with
| `LeftSmallerThanRight, (`Equal | `RightSmallerThanLeft | `RightSubsumesLeft) -> | `LeftSmallerThanRight, (`Equal | `RightSmallerThanLeft | `RightSubsumesLeft) ->
@ -157,7 +157,7 @@ module ArrayAccessCondition = struct
`LeftSubsumesRight `LeftSubsumesRight
| _ -> | _ ->
`NotComparable `NotComparable
else if ItvPure.is_false lidxpos then else if Itv.Boolean.is_false lidxpos then
(* both idx < 0, size doesn't matter *) (* both idx < 0, size doesn't matter *)
match idxcmp with match idxcmp with
| `LeftSmallerThanRight -> | `LeftSmallerThanRight ->
@ -211,9 +211,9 @@ module ArrayAccessCondition = struct
let not_overrun = ItvPure.lt_sem c'.idx c'.size in let not_overrun = ItvPure.lt_sem c'.idx c'.size in
let not_underrun = ItvPure.le_sem ItvPure.zero c'.idx in let not_underrun = ItvPure.le_sem ItvPure.zero c'.idx in
(* il >= 0 and iu < sl, definitely not an error *) (* il >= 0 and iu < sl, definitely not an error *)
if ItvPure.is_one not_overrun && ItvPure.is_one not_underrun then if Itv.Boolean.is_true not_overrun && Itv.Boolean.is_true not_underrun then
{report_issue_type= None; propagate= false} (* iu < 0 or il >= su, definitely an error *) {report_issue_type= None; propagate= false} (* iu < 0 or il >= su, definitely an error *)
else if ItvPure.is_zero not_overrun || ItvPure.is_zero not_underrun then else if Itv.Boolean.is_false not_overrun || Itv.Boolean.is_false not_underrun then
{report_issue_type= Some IssueType.buffer_overrun_l1; propagate= false} {report_issue_type= Some IssueType.buffer_overrun_l1; propagate= false}
(* su <= iu < +oo, most probably an error *) (* su <= iu < +oo, most probably an error *)
else if Itv.Bound.is_not_infty (ItvPure.ub c.idx) else if Itv.Bound.is_not_infty (ItvPure.ub c.idx)

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

@ -32,6 +32,18 @@ module Counter = struct
let next : t -> int = fun counter -> counter () let next : t -> int = fun counter -> counter ()
end end
module Boolean = struct
type t = Bottom | False | True | Top [@@deriving compare]
let top = Top
let equal = [%compare.equal : t]
let is_false = function False -> true | _ -> false
let is_true = function True -> true | _ -> false
end
exception Not_one_symbol exception Not_one_symbol
module Symbol = struct module Symbol = struct
@ -313,8 +325,6 @@ module Bound = struct
type astate = t type astate = t
let equal = [%compare.equal : t]
let pp : F.formatter -> t -> unit = let pp : F.formatter -> t -> unit =
fun fmt -> function fun fmt -> function
| MInf -> | MInf ->
@ -682,16 +692,20 @@ module Bound = struct
let widen_l : t -> t -> t = let widen_l : t -> t -> t =
fun x y -> fun x y ->
if equal x PInf || equal y PInf then L.(die InternalError) "Lower bound cannot be +oo." match (x, y) with
else if le x y then x | PInf, _ | _, PInf ->
else MInf L.(die InternalError) "Lower bound cannot be +oo."
| _ ->
if le x y then x else MInf
let widen_u : t -> t -> t = let widen_u : t -> t -> t =
fun x y -> fun x y ->
if equal x MInf || equal y MInf then L.(die InternalError) "Upper bound cannot be -oo." match (x, y) with
else if le y x then x | MInf, _ | _, MInf ->
else PInf L.(die InternalError) "Upper bound cannot be -oo."
| _ ->
if le y x then x else PInf
let widen ~prev ~next ~num_iters:_ = widen_u prev next let widen ~prev ~next ~num_iters:_ = widen_u prev next
@ -712,8 +726,6 @@ module Bound = struct
let is_zero : t -> bool = is_some_const 0 let is_zero : t -> bool = is_some_const 0
let is_one : t -> bool = is_some_const 1
let is_const : t -> int option = let is_const : t -> int 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
@ -866,8 +878,6 @@ module ItvPure = struct
type t = astate type t = astate
let equal = [%compare.equal : astate]
let lb : t -> Bound.t = fst let lb : t -> Bound.t = fst
let ub : t -> Bound.t = snd let ub : t -> Bound.t = snd
@ -980,8 +990,6 @@ module ItvPure = struct
None None
let is_one : t -> bool = fun (l, u) -> Bound.is_one l && Bound.is_one u
let is_zero : t -> bool = fun (l, u) -> Bound.is_zero l && Bound.is_zero u let is_zero : t -> bool = fun (l, u) -> Bound.is_zero l && Bound.is_zero u
let is_true : t -> bool = fun (l, u) -> Bound.le Bound.one l || Bound.le u Bound.mone let is_true : t -> bool = fun (l, u) -> Bound.le Bound.one l || Bound.le u Bound.mone
@ -1003,8 +1011,8 @@ module ItvPure = struct
(l', u') (l', u')
let lnot : t -> t = let lnot : t -> Boolean.t =
fun x -> if is_true x then false_sem else if is_false x then true_sem else unknown_bool fun x -> if is_true x then Boolean.False else if is_false x then Boolean.True else Boolean.Top
let plus : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.plus_l l1 l2, Bound.plus_u u1 u2) let plus : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.plus_l l1 l2, Bound.plus_u u1 u2)
@ -1099,46 +1107,46 @@ module ItvPure = struct
top top
let lt_sem : t -> t -> t = let lt_sem : t -> t -> Boolean.t =
fun (l1, u1) (l2, u2) -> fun (l1, u1) (l2, u2) ->
if Bound.lt u1 l2 then true_sem else if Bound.le u2 l1 then false_sem else unknown_bool if Bound.lt u1 l2 then Boolean.True else if Bound.le u2 l1 then Boolean.False else Boolean.Top
let gt_sem : t -> t -> t = fun x y -> lt_sem y x let gt_sem : t -> t -> Boolean.t = fun x y -> lt_sem y x
let le_sem : t -> t -> t = let le_sem : t -> t -> Boolean.t =
fun (l1, u1) (l2, u2) -> fun (l1, u1) (l2, u2) ->
if Bound.le u1 l2 then true_sem else if Bound.lt u2 l1 then false_sem else unknown_bool if Bound.le u1 l2 then Boolean.True else if Bound.lt u2 l1 then Boolean.False else Boolean.Top
let ge_sem : t -> t -> t = fun x y -> le_sem y x let ge_sem : t -> t -> Boolean.t = fun x y -> le_sem y x
let eq_sem : t -> t -> t = let eq_sem : t -> t -> Boolean.t =
fun (l1, u1) (l2, u2) -> fun (l1, u1) (l2, u2) ->
if Bound.eq l1 u1 && Bound.eq u1 l2 && Bound.eq l2 u2 then true_sem if Bound.eq l1 u1 && Bound.eq u1 l2 && Bound.eq l2 u2 then Boolean.True
else if Bound.lt u1 l2 || Bound.lt u2 l1 then false_sem else if Bound.lt u1 l2 || Bound.lt u2 l1 then Boolean.False
else unknown_bool else Boolean.Top
let ne_sem : t -> t -> t = let ne_sem : t -> t -> Boolean.t =
fun (l1, u1) (l2, u2) -> fun (l1, u1) (l2, u2) ->
if Bound.eq l1 u1 && Bound.eq u1 l2 && Bound.eq l2 u2 then false_sem if Bound.eq l1 u1 && Bound.eq u1 l2 && Bound.eq l2 u2 then Boolean.False
else if Bound.lt u1 l2 || Bound.lt u2 l1 then true_sem else if Bound.lt u1 l2 || Bound.lt u2 l1 then Boolean.True
else unknown_bool else Boolean.Top
let land_sem : t -> t -> t = let land_sem : t -> t -> Boolean.t =
fun x y -> fun x y ->
if is_true x && is_true y then true_sem if is_true x && is_true y then Boolean.True
else if is_false x || is_false y then false_sem else if is_false x || is_false y then Boolean.False
else unknown_bool else Boolean.Top
let lor_sem : t -> t -> t = let lor_sem : t -> t -> Boolean.t =
fun x y -> fun x y ->
if is_true x || is_true y then true_sem if is_true x || is_true y then Boolean.True
else if is_false x && is_false y then false_sem else if is_false x && is_false y then Boolean.False
else unknown_bool else Boolean.Top
let min_sem : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.lb l1 l2, Bound.lb ~default:u1 u1 u2) let min_sem : t -> t -> t = fun (l1, u1) (l2, u2) -> (Bound.lb l1 l2, Bound.lb ~default:u1 u1 u2)
@ -1302,15 +1310,7 @@ let ub : t -> Bound.t = function
L.(die InternalError) "upper bound of bottom" L.(die InternalError) "upper bound of bottom"
let of_int : int -> astate = fun n -> NonBottom (ItvPure.of_int n) let false_sem = NonBottom ItvPure.false_sem
let of_int_lit n = try of_int (IntLit.to_int n) with _ -> top
let of_int64 : Int64.t -> astate =
fun n -> Int64.to_int n |> Option.value_map ~f:of_int ~default:top
let is_false : t -> bool = function NonBottom x -> ItvPure.is_false x | Bottom -> false
let m1_255 = NonBottom ItvPure.m1_255 let m1_255 = NonBottom ItvPure.m1_255
@ -1320,10 +1320,33 @@ let one = NonBottom ItvPure.one
let pos = NonBottom ItvPure.pos let pos = NonBottom ItvPure.pos
let true_sem = NonBottom ItvPure.true_sem
let unknown_bool = NonBottom ItvPure.unknown_bool let unknown_bool = NonBottom ItvPure.unknown_bool
let zero = NonBottom ItvPure.zero let zero = NonBottom ItvPure.zero
let of_bool = function
| Boolean.Bottom ->
bot
| Boolean.False ->
false_sem
| Boolean.True ->
true_sem
| Boolean.Top ->
unknown_bool
let of_int : int -> astate = fun n -> NonBottom (ItvPure.of_int n)
let of_int_lit n = try of_int (IntLit.to_int n) with _ -> top
let of_int64 : Int64.t -> astate =
fun n -> Int64.to_int n |> Option.value_map ~f:of_int ~default:top
let is_false : t -> bool = function NonBottom x -> ItvPure.is_false x | Bottom -> false
let le : lhs:t -> rhs:t -> bool = ( <= ) let le : lhs:t -> rhs:t -> bool = ( <= )
let eq : t -> t -> bool = fun x y -> ( <= ) ~lhs:x ~rhs:y && ( <= ) ~lhs:y ~rhs:x let eq : t -> t -> bool = fun x y -> ( <= ) ~lhs:x ~rhs:y && ( <= ) ~lhs:y ~rhs:x
@ -1334,7 +1357,13 @@ let lift1 : (ItvPure.t -> ItvPure.t) -> t -> t =
fun f -> function Bottom -> Bottom | NonBottom x -> NonBottom (f x) fun f -> function Bottom -> Bottom | NonBottom x -> NonBottom (f x)
let bind1 : (ItvPure.t -> t) -> t -> t = fun f -> function Bottom -> Bottom | NonBottom x -> f x let bind1_gen : bot:'a -> (ItvPure.t -> 'a) -> t -> 'a =
fun ~bot f x -> match x with Bottom -> bot | NonBottom x -> f x
let bind1 : (ItvPure.t -> t) -> t -> t = bind1_gen ~bot:Bottom
let bind1b : (ItvPure.t -> Boolean.t) -> t -> Boolean.t = bind1_gen ~bot:Boolean.Bottom
let lift2 : (ItvPure.t -> ItvPure.t -> ItvPure.t) -> t -> t -> t = let lift2 : (ItvPure.t -> ItvPure.t -> ItvPure.t) -> t -> t -> t =
fun f x y -> fun f x y ->
@ -1345,9 +1374,15 @@ let lift2 : (ItvPure.t -> ItvPure.t -> ItvPure.t) -> t -> t -> t =
NonBottom (f x y) NonBottom (f x y)
let bind2 : (ItvPure.t -> ItvPure.t -> t) -> t -> t -> t = let bind2_gen : bot:'a -> (ItvPure.t -> ItvPure.t -> 'a) -> t -> t -> 'a =
fun f x y -> fun ~bot f x y ->
match (x, y) with Bottom, _ | _, Bottom -> Bottom | NonBottom x, NonBottom y -> f x y match (x, y) with Bottom, _ | _, Bottom -> bot | NonBottom x, NonBottom y -> f x y
let bind2 : (ItvPure.t -> ItvPure.t -> t) -> t -> t -> t = bind2_gen ~bot:Bottom
let bind2b : (ItvPure.t -> ItvPure.t -> Boolean.t) -> t -> t -> Boolean.t =
bind2_gen ~bot:Boolean.Bottom
let plus : t -> t -> t = lift2 ItvPure.plus let plus : t -> t -> t = lift2 ItvPure.plus
@ -1361,7 +1396,7 @@ let make_sym : ?unsigned:bool -> Typ.Procname.t -> Counter.t -> t =
let neg : t -> t = lift1 ItvPure.neg let neg : t -> t = lift1 ItvPure.neg
let lnot : t -> t = lift1 ItvPure.lnot let lnot : t -> Boolean.t = bind1b ItvPure.lnot
let mult : t -> t -> t = lift2 ItvPure.mult let mult : t -> t -> t = lift2 ItvPure.mult
@ -1373,21 +1408,21 @@ let shiftlt : t -> t -> t = lift2 ItvPure.shiftlt
let shiftrt : t -> t -> t = lift2 ItvPure.shiftrt let shiftrt : t -> t -> t = lift2 ItvPure.shiftrt
let lt_sem : t -> t -> t = lift2 ItvPure.lt_sem let lt_sem : t -> t -> Boolean.t = bind2b ItvPure.lt_sem
let gt_sem : t -> t -> t = lift2 ItvPure.gt_sem let gt_sem : t -> t -> Boolean.t = bind2b ItvPure.gt_sem
let le_sem : t -> t -> t = lift2 ItvPure.le_sem let le_sem : t -> t -> Boolean.t = bind2b ItvPure.le_sem
let ge_sem : t -> t -> t = lift2 ItvPure.ge_sem let ge_sem : t -> t -> Boolean.t = bind2b ItvPure.ge_sem
let eq_sem : t -> t -> t = lift2 ItvPure.eq_sem let eq_sem : t -> t -> Boolean.t = bind2b ItvPure.eq_sem
let ne_sem : t -> t -> t = lift2 ItvPure.ne_sem let ne_sem : t -> t -> Boolean.t = bind2b ItvPure.ne_sem
let land_sem : t -> t -> t = lift2 ItvPure.land_sem let land_sem : t -> t -> Boolean.t = bind2b ItvPure.land_sem
let lor_sem : t -> t -> t = lift2 ItvPure.lor_sem let lor_sem : t -> t -> Boolean.t = bind2b ItvPure.lor_sem
let min_sem : t -> t -> t = lift2 ItvPure.min_sem let min_sem : t -> t -> t = lift2 ItvPure.min_sem

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

@ -19,6 +19,18 @@ module Counter : sig
val next : t -> int val next : t -> int
end end
module Boolean : sig
type t
val top : t
val equal : t -> t -> bool
val is_false : t -> bool
val is_true : t -> bool
end
module Symbol : sig module Symbol : sig
type t type t
end end
@ -84,8 +96,6 @@ module ItvPure : sig
val ub : t -> Bound.t val ub : t -> Bound.t
val is_false : t -> bool
val is_finite : t -> bool val is_finite : t -> bool
val is_invalid : t -> bool val is_invalid : t -> bool
@ -94,20 +104,12 @@ module ItvPure : sig
val is_nat : t -> bool val is_nat : t -> bool
val is_one : t -> bool
val is_symbolic : t -> bool val is_symbolic : t -> bool
val is_top : t -> bool val is_top : t -> bool
val is_true : t -> bool
val is_zero : t -> bool
val ( <= ) : lhs:t -> rhs:t -> bool val ( <= ) : lhs:t -> rhs:t -> bool
val equal : t -> t -> bool
val have_similar_bounds : t -> t -> bool val have_similar_bounds : t -> t -> bool
val has_infty : t -> bool val has_infty : t -> bool
@ -116,9 +118,9 @@ module ItvPure : sig
val join : t -> t -> t val join : t -> t -> t
val le_sem : t -> t -> t val le_sem : t -> t -> Boolean.t
val lt_sem : t -> t -> t val lt_sem : t -> t -> Boolean.t
val widen : prev:t -> next:t -> num_iters:int -> t val widen : prev:t -> next:t -> num_iters:int -> t
@ -158,12 +160,11 @@ val pos : t
val top : t val top : t
(** [-oo, +oo] *) (** [-oo, +oo] *)
val unknown_bool : t
(** [0, 1] *)
val zero : t val zero : t
(** 0 *) (** 0 *)
val of_bool : Boolean.t -> t
val of_int : int -> t val of_int : int -> t
val of_int_lit : IntLit.t -> t val of_int_lit : IntLit.t -> t
@ -178,8 +179,6 @@ val ub : t -> Bound.t
val is_false : t -> bool val is_false : t -> bool
val lnot : t -> t
val neg : t -> t val neg : t -> t
val normalize : t -> t val normalize : t -> t
@ -190,6 +189,8 @@ val eq : t -> t -> bool
val le : lhs:t -> rhs:t -> bool val le : lhs:t -> rhs:t -> bool
val lnot : t -> Boolean.t
val range : t -> Bound.t val range : t -> Bound.t
val div : t -> t -> t val div : t -> t -> t
@ -204,25 +205,25 @@ val shiftlt : t -> t -> t
val shiftrt : t -> t -> t val shiftrt : t -> t -> t
val eq_sem : t -> t -> t val eq_sem : t -> t -> Boolean.t
val ge_sem : t -> t -> t val ge_sem : t -> t -> Boolean.t
val gt_sem : t -> t -> t val gt_sem : t -> t -> Boolean.t
val land_sem : t -> t -> t val land_sem : t -> t -> Boolean.t
val le_sem : t -> t -> t val le_sem : t -> t -> Boolean.t
val lor_sem : t -> t -> t val lor_sem : t -> t -> Boolean.t
val lt_sem : t -> t -> t val lt_sem : t -> t -> Boolean.t
val min_sem : t -> t -> t val min_sem : t -> t -> t
val mod_sem : t -> t -> t val mod_sem : t -> t -> t
val ne_sem : t -> t -> t val ne_sem : t -> t -> Boolean.t
val prune_eq_zero : t -> t val prune_eq_zero : t -> t

Write Preview
Loading…
Cancel
Save