From 52e2fb9f8175566d530132bdfa09485690527383 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Mon, 26 Nov 2018 14:00:58 -0800 Subject: [PATCH] [inferbo] Rename is_collection_add -> last_included Reviewed By: skcho Differential Revision: D13190947 fbshipit-source-id: d435846e8 --- .../src/bufferoverrun/bufferOverrunChecker.ml | 9 ++++-- .../src/bufferoverrun/bufferOverrunModels.ml | 29 +++++++++--------- .../bufferOverrunProofObligations.ml | 26 ++++++++-------- .../bufferOverrunProofObligations.mli | 2 +- infer/src/bufferoverrun/bufferOverrunUtils.ml | 30 ++++++++++--------- .../src/bufferoverrun/bufferOverrunUtils.mli | 5 +++- 6 files changed, 55 insertions(+), 46 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 7ed9c57d5..bb4722af1 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -490,7 +490,8 @@ module Report = struct Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) e2 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 : @@ -524,7 +525,8 @@ module Report = struct match exp with | Exp.Lindex (array_exp, 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) -> cond_set |> check_sub_expr e1 |> check_sub_expr e2 | 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 idx, idx_sym_exp = (Dom.Val.Itv.zero, Some Relation.SymExp.zero) 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) -> check_binop integer_type_widths ~bop ~e1 ~e2 location mem cond_set | _ -> diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index d080b97c4..a112a456a 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -133,10 +133,10 @@ let calloc size_exp stride_exp = let memcpy dest_exp src_exp size_exp = let exec _ ~ret:_ mem = mem 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 - location cond_set + BoUtils.Check.lindex_byte integer_type_widths ~array_exp:dest_exp ~byte_index_exp:size_exp + ~last_included:true mem location cond_set |> BoUtils.Check.lindex_byte integer_type_widths ~array_exp:src_exp ~byte_index_exp:size_exp - mem location + ~last_included:true mem location in {exec; check} @@ -144,8 +144,8 @@ let memcpy dest_exp src_exp size_exp = let memset arr_exp size_exp = let exec _ ~ret:_ mem = mem 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 - location cond_set + BoUtils.Check.lindex_byte integer_type_widths ~array_exp:arr_exp ~byte_index_exp:size_exp + ~last_included:true mem location cond_set in {exec; check} @@ -338,7 +338,8 @@ module StdArray = struct 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 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 {exec; check} @@ -455,8 +456,8 @@ module Collection = struct let add_at_index (alist_id : Ident.t) index_exp = let check {location; integer_type_widths} mem cond_set = let array_exp = Exp.Var alist_id in - BoUtils.Check.collection_access integer_type_widths ~array_exp ~index_exp - ~is_collection_add:true mem location cond_set + BoUtils.Check.collection_access integer_type_widths ~array_exp ~index_exp ~last_included:true + mem location cond_set in {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 check {location; integer_type_widths} mem cond_set = let array_exp = Exp.Var alist_id in - BoUtils.Check.collection_access integer_type_widths ~array_exp ~index_exp mem location - cond_set + BoUtils.Check.collection_access integer_type_widths ~array_exp ~index_exp + ~last_included:false mem location cond_set in {exec= change_size_by ~size_f:decr_size alist_id; check} @@ -477,8 +478,8 @@ module Collection = struct in let check {location; integer_type_widths} mem cond_set = let array_exp = Exp.Var alist_id in - BoUtils.Check.collection_access integer_type_widths ~index_exp ~array_exp - ~is_collection_add:true mem location cond_set + BoUtils.Check.collection_access integer_type_widths ~index_exp ~array_exp ~last_included:true + mem location cond_set in {exec; check} @@ -487,8 +488,8 @@ module Collection = struct let exec _model_env ~ret:_ mem = mem in let check {location; integer_type_widths} mem cond_set = let array_exp = Exp.Var alist_id in - BoUtils.Check.collection_access integer_type_widths ~index_exp ~array_exp mem location - cond_set + BoUtils.Check.collection_access integer_type_widths ~index_exp ~array_exp + ~last_included:false mem location cond_set in {exec; check} end diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 21cdeeaeb..74a769948 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -104,7 +104,7 @@ module ArrayAccessCondition = struct { offset: ItvPure.t ; idx: ItvPure.t ; size: ItvPure.t - ; is_collection_add: bool + ; last_included: bool ; idx_sym_exp: Relation.SymExp.t option ; size_sym_exp: Relation.SymExp.t option ; relation: Relation.t } @@ -120,7 +120,7 @@ module ArrayAccessCondition = struct let pp_offset fmt = if not (ItvPure.is_zero c.offset) then F.fprintf fmt "%a + " ItvPure.pp c.offset 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 (ItvPure.make_positive c.size) ; if Option.is_some Config.bo_relational_domain then @@ -139,7 +139,7 @@ module ArrayAccessCondition = struct (ItvPure.pp_mark ~markup) c.idx in 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) @@ -147,18 +147,18 @@ module ArrayAccessCondition = struct offset:ItvPure.t -> idx:ItvPure.t -> size:ItvPure.t - -> is_collection_add:bool + -> last_included:bool -> idx_sym_exp:Relation.SymExp.t option -> size_sym_exp:Relation.SymExp.t option -> relation:Relation.t -> 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 - 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} - {offset= roff; idx= ridx; size= rsiz; is_collection_add= rcol} = + let have_similar_bounds {offset= loff; idx= lidx; size= lsiz; last_included= lcol} + {offset= roff; idx= ridx; size= rsiz; last_included= rcol} = Bool.equal lcol rcol && ItvPure.have_similar_bounds loff roff && 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 - let xcompare ~lhs:{offset= loff; idx= lidx; size= lsiz; is_collection_add= lcol} - ~rhs:{offset= roff; idx= ridx; size= rsiz; is_collection_add= rcol} = + let xcompare ~lhs:{offset= loff; idx= lidx; size= lsiz; last_included= lcol} + ~rhs:{offset= roff; idx= ridx; size= rsiz; last_included= rcol} = if not (Bool.equal lcol rcol) then `NotComparable else 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 size = 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 (* if sl < 0, use sl' = 0 *) let not_overrun = @@ -817,9 +817,9 @@ module ConditionSet = struct 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 = - 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 |> Condition.make_array_access |> add_opt location diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli index 49de0edea..0167fb418 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.mli +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.mli @@ -38,7 +38,7 @@ module ConditionSet : sig -> offset:ItvPure.t -> idx:ItvPure.t -> size:ItvPure.t - -> is_collection_add:bool + -> last_included:bool -> idx_sym_exp:Relation.SymExp.t option -> size_sym_exp:Relation.SymExp.t option -> relation:Relation.t diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 3ef02f293..cfe2fc01e 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -291,8 +291,8 @@ module Exec = struct end module Check = struct - let check_access ~size ~idx ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces - ?(is_collection_add = false) location cond_set = + let check_access ~size ~idx ~size_sym_exp ~idx_sym_exp ~relation ~arr ~idx_traces ~last_included + location cond_set = match (size, idx) with | NonBottom length, NonBottom idx -> let offset = @@ -305,12 +305,12 @@ module Check = struct in let arr_traces = Dom.Val.get_traces arr in 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 - 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 size = ArrayBlk.sizeof arr_blk 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) "@[Add condition :@,array: %a@, idx: %a + %a@,@]@." ArrayBlk.pp arr_blk Itv.pp (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 - location cond_set = + let collection_access 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 arr = Sem.eval integer_type_widths array_exp mem 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 relation = Dom.Mem.get_relation mem in 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 arr = Sem.eval_arr integer_type_widths array_exp mem in let idx_sym_exp = Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) index_exp 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 size = ArrayBlk.sizeof_byte arr_blk in let idx_itv = Dom.Val.get_itv idx in @@ -361,14 +362,15 @@ module Check = struct "@[Add condition :@,array: %a@, idx: %a + %a@,@]@." ArrayBlk.pp arr_blk Itv.pp (ArrayBlk.offsetof arr_blk) Itv.pp idx ; 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 arr = Sem.eval_arr integer_type_widths array_exp 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 = diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index d1502ea6b..bfd98483d 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -134,6 +134,7 @@ module Check : sig -> idx_sym_exp:Relation.SymExp.t option -> relation:Relation.t -> is_plus:bool + -> last_included:bool -> Location.t -> PO.ConditionSet.t -> PO.ConditionSet.t @@ -142,6 +143,7 @@ module Check : sig Typ.IntegerWidths.t -> array_exp:Exp.t -> index_exp:Exp.t + -> last_included:bool -> Dom.Mem.t -> Location.t -> PO.ConditionSet.t @@ -151,6 +153,7 @@ module Check : sig Typ.IntegerWidths.t -> array_exp:Exp.t -> byte_index_exp:Exp.t + -> last_included:bool -> Dom.Mem.t -> Location.t -> PO.ConditionSet.t @@ -160,7 +163,7 @@ module Check : sig Typ.IntegerWidths.t -> array_exp:Exp.t -> index_exp:Exp.t - -> ?is_collection_add:bool + -> last_included:bool -> Dom.Mem.t -> Location.t -> PO.ConditionSet.t