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

[inferbo] Rename is_collection_add -> last_included

Browse Source 
Reviewed By: skcho

Differential Revision: D13190947

fbshipit-source-id: d435846e8
master
Mehdi Bouaziz 6 years ago committed by Facebook Github Bot
parent b92800a716
commit 52e2fb9f81
6 changed files with 55 additions and 46 deletions
Show Stats Download Patch File Download Diff File

9
infer/src/bufferoverrun/bufferOverrunChecker.ml
Unescape View File

@ -490,7 +490,8 @@ module Report = struct
Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) e2 Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) e2
in in
let relation = Dom.Mem.get_relation mem in let relation = Dom.Mem.get_relation mem in
BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus location cond_set BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus ~last_included:false
location cond_set
let check_binop : let check_binop :
@ -524,7 +525,8 @@ module Report = struct
match exp with match exp with
| Exp.Lindex (array_exp, index_exp) -> | Exp.Lindex (array_exp, index_exp) ->
cond_set |> check_sub_expr array_exp |> check_sub_expr index_exp cond_set |> check_sub_expr array_exp |> check_sub_expr index_exp
|> BoUtils.Check.lindex integer_type_widths ~array_exp ~index_exp mem location |> BoUtils.Check.lindex integer_type_widths ~array_exp ~index_exp ~last_included:false
mem location
| Exp.BinOp (_, e1, e2) -> | Exp.BinOp (_, e1, e2) ->
cond_set |> check_sub_expr e1 |> check_sub_expr e2 cond_set |> check_sub_expr e1 |> check_sub_expr e2
| Exp.Lfield (e, _, _) | Exp.UnOp (_, e, _) | Exp.Exn e -> | Exp.Lfield (e, _, _) | Exp.UnOp (_, e, _) | Exp.Exn e ->
@ -543,7 +545,8 @@ module Report = struct
let arr = Sem.eval integer_type_widths exp mem in let arr = Sem.eval integer_type_widths exp mem in
let idx, idx_sym_exp = (Dom.Val.Itv.zero, Some Relation.SymExp.zero) in let idx, idx_sym_exp = (Dom.Val.Itv.zero, Some Relation.SymExp.zero) in
let relation = Dom.Mem.get_relation mem in let relation = Dom.Mem.get_relation mem in
BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true location cond_set BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true
~last_included:false location cond_set
| Exp.BinOp (bop, e1, e2) -> | Exp.BinOp (bop, e1, e2) ->
check_binop integer_type_widths ~bop ~e1 ~e2 location mem cond_set check_binop integer_type_widths ~bop ~e1 ~e2 location mem cond_set
| _ -> | _ ->

29
infer/src/bufferoverrun/bufferOverrunModels.ml
Unescape View File

@ -133,10 +133,10 @@ let calloc size_exp stride_exp =
let memcpy dest_exp src_exp size_exp = let memcpy dest_exp src_exp size_exp =
let exec _ ~ret:_ mem = mem let exec _ ~ret:_ mem = mem
and check {location; integer_type_widths} mem cond_set = and check {location; integer_type_widths} mem cond_set =
BoUtils.Check.lindex_byte integer_type_widths ~array_exp:dest_exp ~byte_index_exp:size_exp mem BoUtils.Check.lindex_byte integer_type_widths ~array_exp:dest_exp ~byte_index_exp:size_exp
location cond_set ~last_included:true mem location cond_set
|> BoUtils.Check.lindex_byte integer_type_widths ~array_exp:src_exp ~byte_index_exp:size_exp |> BoUtils.Check.lindex_byte integer_type_widths ~array_exp:src_exp ~byte_index_exp:size_exp
mem location ~last_included:true mem location
in in
{exec; check} {exec; check}
@ -144,8 +144,8 @@ let memcpy dest_exp src_exp size_exp =
let memset arr_exp size_exp = let memset arr_exp size_exp =
let exec _ ~ret:_ mem = mem let exec _ ~ret:_ mem = mem
and check {location; integer_type_widths} mem cond_set = and check {location; integer_type_widths} mem cond_set =
BoUtils.Check.lindex_byte integer_type_widths ~array_exp:arr_exp ~byte_index_exp:size_exp mem BoUtils.Check.lindex_byte integer_type_widths ~array_exp:arr_exp ~byte_index_exp:size_exp
location cond_set ~last_included:true mem location cond_set
in in
{exec; check} {exec; check}
@ -338,7 +338,8 @@ module StdArray = struct
L.d_printfln_escaped "Using model std::array<_, %Ld>::at" _size ; L.d_printfln_escaped "Using model std::array<_, %Ld>::at" _size ;
BoUtils.Exec.load_val id (Sem.eval_lindex integer_type_widths array_exp index_exp mem) mem BoUtils.Exec.load_val id (Sem.eval_lindex integer_type_widths array_exp index_exp mem) mem
and check {location; integer_type_widths} mem cond_set = and check {location; integer_type_widths} mem cond_set =
BoUtils.Check.lindex integer_type_widths ~array_exp ~index_exp mem location cond_set BoUtils.Check.lindex integer_type_widths ~array_exp ~index_exp ~last_included:false mem
location cond_set
in in
{exec; check} {exec; check}
@ -455,8 +456,8 @@ module Collection = struct
let add_at_index (alist_id : Ident.t) index_exp = let add_at_index (alist_id : Ident.t) index_exp =
let check {location; integer_type_widths} mem cond_set = let check {location; integer_type_widths} mem cond_set =
let array_exp = Exp.Var alist_id in let array_exp = Exp.Var alist_id in
BoUtils.Check.collection_access integer_type_widths ~array_exp ~index_exp BoUtils.Check.collection_access integer_type_widths ~array_exp ~index_exp ~last_included:true
~is_collection_add:true mem location cond_set mem location cond_set
in in
{exec= change_size_by ~size_f:incr_size alist_id; check} {exec= change_size_by ~size_f:incr_size alist_id; check}
@ -464,8 +465,8 @@ module Collection = struct
let remove_at_index alist_id index_exp = let remove_at_index alist_id index_exp =
let check {location; integer_type_widths} mem cond_set = let check {location; integer_type_widths} mem cond_set =
let array_exp = Exp.Var alist_id in let array_exp = Exp.Var alist_id in
BoUtils.Check.collection_access integer_type_widths ~array_exp ~index_exp mem location BoUtils.Check.collection_access integer_type_widths ~array_exp ~index_exp
cond_set ~last_included:false mem location cond_set
in in
{exec= change_size_by ~size_f:decr_size alist_id; check} {exec= change_size_by ~size_f:decr_size alist_id; check}
@ -477,8 +478,8 @@ module Collection = struct
in in
let check {location; integer_type_widths} mem cond_set = let check {location; integer_type_widths} mem cond_set =
let array_exp = Exp.Var alist_id in let array_exp = Exp.Var alist_id in
BoUtils.Check.collection_access integer_type_widths ~index_exp ~array_exp BoUtils.Check.collection_access integer_type_widths ~index_exp ~array_exp ~last_included:true
~is_collection_add:true mem location cond_set mem location cond_set
in in
{exec; check} {exec; check}
@ -487,8 +488,8 @@ module Collection = struct
let exec _model_env ~ret:_ mem = mem in let exec _model_env ~ret:_ mem = mem in
let check {location; integer_type_widths} mem cond_set = let check {location; integer_type_widths} mem cond_set =
let array_exp = Exp.Var alist_id in let array_exp = Exp.Var alist_id in
BoUtils.Check.collection_access integer_type_widths ~index_exp ~array_exp mem location BoUtils.Check.collection_access integer_type_widths ~index_exp ~array_exp
cond_set ~last_included:false mem location cond_set
in in
{exec; check} {exec; check}
end end

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

@ -104,7 +104,7 @@ module ArrayAccessCondition = struct
{ offset: ItvPure.t { offset: ItvPure.t
; idx: ItvPure.t ; idx: ItvPure.t
; size: ItvPure.t ; size: ItvPure.t
; is_collection_add: bool ; last_included: bool
; idx_sym_exp: Relation.SymExp.t option ; idx_sym_exp: Relation.SymExp.t option
; size_sym_exp: Relation.SymExp.t option ; size_sym_exp: Relation.SymExp.t option
; relation: Relation.t } ; relation: Relation.t }
@ -120,7 +120,7 @@ module ArrayAccessCondition = struct
let pp_offset fmt = let pp_offset fmt =
if not (ItvPure.is_zero c.offset) then F.fprintf fmt "%a + " ItvPure.pp c.offset if not (ItvPure.is_zero c.offset) then F.fprintf fmt "%a + " ItvPure.pp c.offset
in in
let cmp = if c.is_collection_add then "<=" else "<" in let cmp = if c.last_included then "<=" else "<" in
F.fprintf fmt "%t%a %s %a" pp_offset ItvPure.pp c.idx cmp ItvPure.pp F.fprintf fmt "%t%a %s %a" pp_offset ItvPure.pp c.idx cmp ItvPure.pp
(ItvPure.make_positive c.size) ; (ItvPure.make_positive c.size) ;
if Option.is_some Config.bo_relational_domain then if Option.is_some Config.bo_relational_domain then
@ -139,7 +139,7 @@ module ArrayAccessCondition = struct
(ItvPure.pp_mark ~markup) c.idx (ItvPure.pp_mark ~markup) c.idx
in in
F.fprintf fmt "Offset%s: %t Size: %a" F.fprintf fmt "Offset%s: %t Size: %a"
(if c.is_collection_add then " added" else "") (if c.last_included then " added" else "")
pp_offset (ItvPure.pp_mark ~markup) (ItvPure.make_positive c.size) pp_offset (ItvPure.pp_mark ~markup) (ItvPure.make_positive c.size)
@ -147,18 +147,18 @@ module ArrayAccessCondition = struct
offset:ItvPure.t offset:ItvPure.t
-> idx:ItvPure.t -> idx:ItvPure.t
-> size:ItvPure.t -> size:ItvPure.t
-> is_collection_add:bool -> last_included:bool
-> idx_sym_exp:Relation.SymExp.t option -> idx_sym_exp:Relation.SymExp.t option
-> size_sym_exp:Relation.SymExp.t option -> size_sym_exp:Relation.SymExp.t option
-> relation:Relation.t -> relation:Relation.t
-> t option = -> t option =
fun ~offset ~idx ~size ~is_collection_add ~idx_sym_exp ~size_sym_exp ~relation -> fun ~offset ~idx ~size ~last_included ~idx_sym_exp ~size_sym_exp ~relation ->
if ItvPure.is_invalid offset || ItvPure.is_invalid idx || ItvPure.is_invalid size then None if ItvPure.is_invalid offset || ItvPure.is_invalid idx || ItvPure.is_invalid size then None
else Some {offset; idx; size; is_collection_add; idx_sym_exp; size_sym_exp; relation} else Some {offset; idx; size; last_included; idx_sym_exp; size_sym_exp; relation}
let have_similar_bounds {offset= loff; idx= lidx; size= lsiz; is_collection_add= lcol} let have_similar_bounds {offset= loff; idx= lidx; size= lsiz; last_included= lcol}
{offset= roff; idx= ridx; size= rsiz; is_collection_add= rcol} = {offset= roff; idx= ridx; size= rsiz; last_included= rcol} =
Bool.equal lcol rcol Bool.equal lcol rcol
&& ItvPure.have_similar_bounds loff roff && ItvPure.have_similar_bounds loff roff
&& ItvPure.have_similar_bounds lidx ridx && ItvPure.have_similar_bounds lidx ridx
@ -169,8 +169,8 @@ module ArrayAccessCondition = struct
ItvPure.has_infty offset || ItvPure.has_infty idx || ItvPure.has_infty size ItvPure.has_infty offset || ItvPure.has_infty idx || ItvPure.has_infty size
let xcompare ~lhs:{offset= loff; idx= lidx; size= lsiz; is_collection_add= lcol} let xcompare ~lhs:{offset= loff; idx= lidx; size= lsiz; last_included= lcol}
~rhs:{offset= roff; idx= ridx; size= rsiz; is_collection_add= rcol} = ~rhs:{offset= roff; idx= ridx; size= rsiz; last_included= rcol} =
if not (Bool.equal lcol rcol) then `NotComparable if not (Bool.equal lcol rcol) then `NotComparable
else else
let offcmp = ItvPure.xcompare ~lhs:loff ~rhs:roff in let offcmp = ItvPure.xcompare ~lhs:loff ~rhs:roff in
@ -264,7 +264,7 @@ module ArrayAccessCondition = struct
let real_idx = ItvPure.plus c.offset c.idx in let real_idx = ItvPure.plus c.offset c.idx in
let size = let size =
let size_pos = ItvPure.make_positive c.size in let size_pos = ItvPure.make_positive c.size in
if c.is_collection_add then ItvPure.succ size_pos else size_pos if c.last_included then ItvPure.succ size_pos else size_pos
in in
(* if sl < 0, use sl' = 0 *) (* if sl < 0, use sl' = 0 *)
let not_overrun = let not_overrun =
@ -817,9 +817,9 @@ module ConditionSet = struct
join [cwt] condset join [cwt] condset
let add_array_access location ~offset ~idx ~size ~is_collection_add ~idx_sym_exp ~size_sym_exp let add_array_access location ~offset ~idx ~size ~last_included ~idx_sym_exp ~size_sym_exp
~relation ~idx_traces ~arr_traces condset = ~relation ~idx_traces ~arr_traces condset =
ArrayAccessCondition.make ~offset ~idx ~size ~is_collection_add ~idx_sym_exp ~size_sym_exp ArrayAccessCondition.make ~offset ~idx ~size ~last_included ~idx_sym_exp ~size_sym_exp
~relation ~relation
|> Condition.make_array_access |> Condition.make_array_access
|> add_opt location |> add_opt location

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

@ -38,7 +38,7 @@ module ConditionSet : sig
-> offset:ItvPure.t -> offset:ItvPure.t
-> idx:ItvPure.t -> idx:ItvPure.t
-> size:ItvPure.t -> size:ItvPure.t
-> is_collection_add:bool -> last_included:bool
-> idx_sym_exp:Relation.SymExp.t option -> idx_sym_exp:Relation.SymExp.t option
-> size_sym_exp:Relation.SymExp.t option -> size_sym_exp:Relation.SymExp.t option
-> relation:Relation.t -> relation:Relation.t

30
infer/src/bufferoverrun/bufferOverrunUtils.ml
Unescape View File

@ -291,8 +291,8 @@ module Exec = struct
end end
module Check = struct module Check = struct
let check_access ~size ~idx ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces let check_access ~size ~idx ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces ~last_included
?(is_collection_add = false) location cond_set = location cond_set =
match (size, idx) with match (size, idx) with
| NonBottom length, NonBottom idx -> | NonBottom length, NonBottom idx ->
let offset = let offset =
@ -305,12 +305,12 @@ module Check = struct
in in
let arr_traces = Dom.Val.get_traces arr in let arr_traces = Dom.Val.get_traces arr in
PO.ConditionSet.add_array_access location ~size:length ~offset ~idx ~size_sym_exp PO.ConditionSet.add_array_access location ~size:length ~offset ~idx ~size_sym_exp
~idx_sym_exp ~relation ~is_collection_add ~idx_traces ~arr_traces cond_set ~idx_sym_exp ~relation ~last_included ~idx_traces ~arr_traces cond_set
| _ -> | _ ->
cond_set cond_set
let array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus location cond_set = let array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus ~last_included location cond_set =
let arr_blk = Dom.Val.get_array_blk arr in let arr_blk = Dom.Val.get_array_blk arr in
let size = ArrayBlk.sizeof arr_blk in let size = ArrayBlk.sizeof arr_blk in
let size_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_size_sym arr) in let size_sym_exp = Relation.SymExp.of_sym (Dom.Val.get_size_sym arr) in
@ -326,11 +326,12 @@ module Check = struct
L.(debug BufferOverrun Verbose) L.(debug BufferOverrun Verbose)
"@[<v 2>Add condition :@,array: %a@, idx: %a + %a@,@]@." ArrayBlk.pp arr_blk Itv.pp "@[<v 2>Add condition :@,array: %a@, idx: %a + %a@,@]@." ArrayBlk.pp arr_blk Itv.pp
(ArrayBlk.offsetof arr_blk) Itv.pp idx ; (ArrayBlk.offsetof arr_blk) Itv.pp idx ;
check_access ~size ~idx ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces location cond_set check_access ~size ~idx ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces ~last_included
location cond_set
let collection_access integer_type_widths ~array_exp ~index_exp ?(is_collection_add = false) mem let collection_access integer_type_widths ~array_exp ~index_exp ~last_included mem location
location cond_set = cond_set =
let idx = Sem.eval integer_type_widths index_exp mem in let idx = Sem.eval integer_type_widths index_exp mem in
let arr = Sem.eval integer_type_widths array_exp mem in let arr = Sem.eval integer_type_widths array_exp mem in
let idx_traces = Dom.Val.get_traces idx in let idx_traces = Dom.Val.get_traces idx in
@ -338,20 +339,20 @@ module Check = struct
let idx = Dom.Val.get_itv idx in let idx = Dom.Val.get_itv idx in
let relation = Dom.Mem.get_relation mem in let relation = Dom.Mem.get_relation mem in
check_access ~size ~idx ~size_sym_exp:None ~idx_sym_exp:None ~relation ~arr ~idx_traces check_access ~size ~idx ~size_sym_exp:None ~idx_sym_exp:None ~relation ~arr ~idx_traces
~is_collection_add location cond_set ~last_included location cond_set
let lindex integer_type_widths ~array_exp ~index_exp mem location cond_set = let lindex integer_type_widths ~array_exp ~index_exp ~last_included mem location cond_set =
let idx = Sem.eval integer_type_widths index_exp mem in let idx = Sem.eval integer_type_widths index_exp mem in
let arr = Sem.eval_arr integer_type_widths array_exp mem in let arr = Sem.eval_arr integer_type_widths array_exp mem in
let idx_sym_exp = let idx_sym_exp =
Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) index_exp Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) index_exp
in in
let relation = Dom.Mem.get_relation mem in let relation = Dom.Mem.get_relation mem in
array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true location cond_set array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true ~last_included location cond_set
let array_access_byte ~arr ~idx ~relation ~is_plus location cond_set = let array_access_byte ~arr ~idx ~relation ~is_plus ~last_included location cond_set =
let arr_blk = Dom.Val.get_array_blk arr in let arr_blk = Dom.Val.get_array_blk arr in
let size = ArrayBlk.sizeof_byte arr_blk in let size = ArrayBlk.sizeof_byte arr_blk in
let idx_itv = Dom.Val.get_itv idx in let idx_itv = Dom.Val.get_itv idx in
@ -361,14 +362,15 @@ module Check = struct
"@[<v 2>Add condition :@,array: %a@, idx: %a + %a@,@]@." ArrayBlk.pp arr_blk Itv.pp "@[<v 2>Add condition :@,array: %a@, idx: %a + %a@,@]@." ArrayBlk.pp arr_blk Itv.pp
(ArrayBlk.offsetof arr_blk) Itv.pp idx ; (ArrayBlk.offsetof arr_blk) Itv.pp idx ;
check_access ~size ~idx ~size_sym_exp:None ~idx_sym_exp:None ~relation ~arr ~idx_traces check_access ~size ~idx ~size_sym_exp:None ~idx_sym_exp:None ~relation ~arr ~idx_traces
location cond_set ~is_collection_add:true ~last_included location cond_set
let lindex_byte integer_type_widths ~array_exp ~byte_index_exp mem location cond_set = let lindex_byte integer_type_widths ~array_exp ~byte_index_exp ~last_included mem location
cond_set =
let idx = Sem.eval integer_type_widths byte_index_exp mem in let idx = Sem.eval integer_type_widths byte_index_exp mem in
let arr = Sem.eval_arr integer_type_widths array_exp mem in let arr = Sem.eval_arr integer_type_widths array_exp mem in
let relation = Dom.Mem.get_relation mem in let relation = Dom.Mem.get_relation mem in
array_access_byte ~arr ~idx ~relation ~is_plus:true location cond_set array_access_byte ~arr ~idx ~relation ~is_plus:true ~last_included location cond_set
let binary_operation integer_type_widths bop ~lhs ~rhs location cond_set = let binary_operation integer_type_widths bop ~lhs ~rhs location cond_set =

5
infer/src/bufferoverrun/bufferOverrunUtils.mli
Unescape View File

@ -134,6 +134,7 @@ module Check : sig
-> idx_sym_exp:Relation.SymExp.t option -> idx_sym_exp:Relation.SymExp.t option
-> relation:Relation.t -> relation:Relation.t
-> is_plus:bool -> is_plus:bool
-> last_included:bool
-> Location.t -> Location.t
-> PO.ConditionSet.t -> PO.ConditionSet.t
-> PO.ConditionSet.t -> PO.ConditionSet.t
@ -142,6 +143,7 @@ module Check : sig
Typ.IntegerWidths.t Typ.IntegerWidths.t
-> array_exp:Exp.t -> array_exp:Exp.t
-> index_exp:Exp.t -> index_exp:Exp.t
-> last_included:bool
-> Dom.Mem.t -> Dom.Mem.t
-> Location.t -> Location.t
-> PO.ConditionSet.t -> PO.ConditionSet.t
@ -151,6 +153,7 @@ module Check : sig
Typ.IntegerWidths.t Typ.IntegerWidths.t
-> array_exp:Exp.t -> array_exp:Exp.t
-> byte_index_exp:Exp.t -> byte_index_exp:Exp.t
-> last_included:bool
-> Dom.Mem.t -> Dom.Mem.t
-> Location.t -> Location.t
-> PO.ConditionSet.t -> PO.ConditionSet.t
@ -160,7 +163,7 @@ module Check : sig
Typ.IntegerWidths.t Typ.IntegerWidths.t
-> array_exp:Exp.t -> array_exp:Exp.t
-> index_exp:Exp.t -> index_exp:Exp.t
-> ?is_collection_add:bool -> last_included:bool
-> Dom.Mem.t -> Dom.Mem.t
-> Location.t -> Location.t
-> PO.ConditionSet.t -> PO.ConditionSet.t

Write Preview
Loading…
Cancel
Save