From 29631b7358bee6b130649c61beea4af89860376c Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Fri, 16 Nov 2018 10:36:56 -0800 Subject: [PATCH] [Inferbo] Differentiate array and pointer in SymbolPaths Reviewed By: jvillard Differential Revision: D12939124 fbshipit-source-id: 256d0b159 --- infer/src/bufferoverrun/bufferOverrunChecker.ml | 6 +++--- infer/src/bufferoverrun/bufferOverrunModels.ml | 6 +++--- infer/src/bufferoverrun/bufferOverrunSemantics.ml | 2 +- infer/src/bufferoverrun/bufferOverrunUtils.ml | 6 ++---- infer/src/bufferoverrun/bufferOverrunUtils.mli | 4 +--- infer/src/bufferoverrun/symb.ml | 11 ++++++++--- infer/src/bufferoverrun/symb.mli | 9 +++++++-- 7 files changed, 25 insertions(+), 19 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 275dca665..cdd608367 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -304,7 +304,7 @@ module Init = struct | {desc= Typ.Tarray {elt}} -> BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field:false) - BoUtils.Exec.CSymArray_Array pname symbol_table path tenv ~node_hash location + Symb.SymbolPath.CSymArray_Array pname symbol_table path tenv ~node_hash location ~represents_multiple_values ~depth loc elt ~inst_num ~new_sym_num ~new_alloc_num mem | _ -> @@ -314,7 +314,7 @@ module Init = struct ~inst_num ~new_alloc_num mem ) | Typ.Tptr (typ, _) -> BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field) - BoUtils.Exec.CSymArray_Pointer pname symbol_table path tenv ~node_hash location + Symb.SymbolPath.CSymArray_Pointer pname symbol_table path tenv ~node_hash location ~represents_multiple_values ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem | Typ.Tarray {elt; length; stride} -> let size = @@ -328,7 +328,7 @@ module Init = struct let stride = Option.map ~f:IntLit.to_int_exn stride in BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field:false) - BoUtils.Exec.CSymArray_Array pname symbol_table path tenv ~node_hash location + Symb.SymbolPath.CSymArray_Array pname symbol_table path tenv ~node_hash location ~represents_multiple_values ~depth loc elt ~offset ?size ?stride ~inst_num ~new_sym_num ~new_alloc_num mem | Typ.Tstruct typename -> ( diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 41313e4e5..6721d1333 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -320,9 +320,9 @@ module StdArray = struct ~represents_multiple_values ~depth loc ~inst_num ~new_sym_num ~new_alloc_num mem = let offset = Itv.zero in let size = Itv.of_int64 length in - BoUtils.Exec.decl_sym_arr ~decl_sym_val BoUtils.Exec.CSymArray_Array pname symbol_table path - tenv ~node_hash location ~represents_multiple_values ~depth loc typ ~offset ~size ~inst_num - ~new_sym_num ~new_alloc_num mem + BoUtils.Exec.decl_sym_arr ~decl_sym_val Symb.SymbolPath.CSymArray_Array pname symbol_table + path tenv ~node_hash location ~represents_multiple_values ~depth loc typ ~offset ~size + ~inst_num ~new_sym_num ~new_alloc_num mem in {declare_local; declare_symbolic} diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 06fe64ffe..773379b46 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -313,7 +313,7 @@ and eval_locpath params p mem = | Symb.SymbolPath.Pvar _ -> let v = eval_sympath_partial params p mem in Val.get_all_locs v - | Symb.SymbolPath.Index p -> + | Symb.SymbolPath.Index (_, p) -> let v = eval_sympath_partial params p mem in Val.get_all_locs v | Symb.SymbolPath.Field (fn, p) -> diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index c2cf0ca06..a75c13099 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -112,8 +112,6 @@ module Exec = struct (mem, inst_num + 1) - type c_sym_array_kind = CSymArray_Array | CSymArray_Pointer - type decl_sym_val = Typ.Procname.t -> Itv.SymbolPath.partial @@ -129,7 +127,7 @@ module Exec = struct let decl_sym_arr : decl_sym_val:decl_sym_val - -> c_sym_array_kind + -> Symb.SymbolPath.c_sym_array_kind -> Typ.Procname.t -> Itv.SymbolTable.t -> Itv.SymbolPath.partial @@ -161,7 +159,7 @@ module Exec = struct Itv.make_sym ~unsigned:true pname symbol_table (Itv.SymbolPath.length path) new_sym_num ) in - let deref_path = Itv.SymbolPath.index path in + let deref_path = Itv.SymbolPath.index ~array_kind path in let allocsite = let alloc_num = Itv.Counter.next new_alloc_num in Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num ~path:(Some deref_path) diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index a883a5062..32daea9a9 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -67,11 +67,9 @@ module Exec : sig -> Dom.Mem.astate -> Dom.Mem.astate - type c_sym_array_kind = CSymArray_Array | CSymArray_Pointer - val decl_sym_arr : decl_sym_val:decl_sym_val - -> c_sym_array_kind + -> Symb.SymbolPath.c_sym_array_kind -> Typ.Procname.t -> Itv.SymbolTable.t -> Itv.SymbolPath.partial diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index ca061abc7..f389da767 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/infer/src/bufferoverrun/symb.ml @@ -16,7 +16,12 @@ module BoundEnd = struct end module SymbolPath = struct - type partial = Pvar of Pvar.t | Index of partial | Field of Typ.Fieldname.t * partial + type c_sym_array_kind = CSymArray_Array | CSymArray_Pointer [@@deriving compare] + + type partial = + | Pvar of Pvar.t + | Index of c_sym_array_kind * partial + | Field of Typ.Fieldname.t * partial [@@deriving compare] type t = Normal of partial | Offset of partial | Length of partial [@@deriving compare] @@ -27,7 +32,7 @@ module SymbolPath = struct let field p fn = Field (fn, p) - let index p = Index p + let index ~array_kind p = Index (array_kind, p) let normal p = Normal p @@ -38,7 +43,7 @@ module SymbolPath = struct let rec pp_partial fmt = function | Pvar pvar -> Pvar.pp_value fmt pvar - | Index p -> + | Index (_, p) -> F.fprintf fmt "%a[*]" pp_partial p | Field (fn, p) -> F.fprintf fmt "%a.%s" pp_partial p (Typ.Fieldname.to_flat_string fn) diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index 745e58821..d32a6e48e 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/infer/src/bufferoverrun/symb.mli @@ -15,7 +15,12 @@ module BoundEnd : sig end module SymbolPath : sig - type partial = private Pvar of Pvar.t | Index of partial | Field of Typ.Fieldname.t * partial + type c_sym_array_kind = CSymArray_Array | CSymArray_Pointer [@@deriving compare] + + type partial = private + | Pvar of Pvar.t + | Index of c_sym_array_kind * partial + | Field of Typ.Fieldname.t * partial [@@deriving compare] type t = private Normal of partial | Offset of partial | Length of partial @@ -24,7 +29,7 @@ module SymbolPath : sig val of_pvar : Pvar.t -> partial - val index : partial -> partial + val index : array_kind:c_sym_array_kind -> partial -> partial val field : partial -> Typ.Fieldname.t -> partial