From 1f96fd03ccff4614a243f85a1f6c16f38c99eb42 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Thu, 22 Nov 2018 11:24:56 -0800 Subject: [PATCH] [inferbo] SymbolPath: rename Index -> Deref Reviewed By: ezgicicek Differential Revision: D13128441 fbshipit-source-id: f6547ed7c --- infer/src/bufferoverrun/bufferOverrunChecker.ml | 6 +++--- infer/src/bufferoverrun/bufferOverrunModels.ml | 2 +- infer/src/bufferoverrun/bufferOverrunSemantics.ml | 4 ++-- infer/src/bufferoverrun/bufferOverrunUtils.ml | 6 +++--- infer/src/bufferoverrun/bufferOverrunUtils.mli | 2 +- infer/src/bufferoverrun/symb.ml | 12 ++++++------ infer/src/bufferoverrun/symb.mli | 6 +++--- 7 files changed, 19 insertions(+), 19 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 0a1b4c27f..354365f69 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -310,7 +310,7 @@ module Init = struct | {desc= Typ.Tarray {elt}} -> BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field:false) - Symb.SymbolPath.CSymArray_Array pname symbol_table path tenv ~node_hash location + Symb.SymbolPath.Deref_ArrayIndex pname symbol_table path tenv ~node_hash location ~depth loc elt ~inst_num ~new_sym_num ~new_alloc_num mem | _ -> BoUtils.Exec.decl_sym_java_ptr @@ -318,7 +318,7 @@ module Init = struct pname path tenv ~node_hash location ~depth loc typ ~inst_num ~new_alloc_num mem ) | Typ.Tptr (typ, _) -> BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field) - Symb.SymbolPath.CSymArray_Pointer pname symbol_table path tenv ~node_hash location + Symb.SymbolPath.Deref_CPointer pname symbol_table path tenv ~node_hash location ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem | Typ.Tarray {elt; length; stride} -> let size = @@ -332,7 +332,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) - Symb.SymbolPath.CSymArray_Array pname symbol_table path tenv ~node_hash location + Symb.SymbolPath.Deref_ArrayIndex pname symbol_table path tenv ~node_hash location ~depth loc elt ~offset ?size ?stride ~inst_num ~new_sym_num ~new_alloc_num mem | Typ.Tstruct typename -> ( match Models.TypName.dispatch tenv typename with diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 2e755aa16..2ad01a621 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -324,7 +324,7 @@ module StdArray = struct 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 Symb.SymbolPath.CSymArray_Array pname symbol_table + BoUtils.Exec.decl_sym_arr ~decl_sym_val Symb.SymbolPath.Deref_ArrayIndex pname symbol_table path tenv ~node_hash location ~depth loc typ ~offset ~size ~inst_num ~new_sym_num ~new_alloc_num mem in diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 050175578..40c2a66b2 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -318,7 +318,7 @@ let rec eval_sympath_partial params p mem = L.(debug BufferOverrun Verbose) "Symbol %a is not found in parameters.@\n" (Pvar.pp Pp.text) x ; Val.Itv.top ) - | Symb.SymbolPath.Index _ | Symb.SymbolPath.Field _ -> + | Symb.SymbolPath.Deref _ | Symb.SymbolPath.Field _ -> let locs = eval_locpath params p mem in Mem.find_set locs mem @@ -328,7 +328,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.Deref (_, 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 a67f92c57..bd014dbdb 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -126,7 +126,7 @@ module Exec = struct let decl_sym_arr : decl_sym_val:decl_sym_val - -> Symb.SymbolPath.c_sym_array_kind + -> Symb.SymbolPath.deref_kind -> Typ.Procname.t -> Itv.SymbolTable.t -> Itv.SymbolPath.partial @@ -144,7 +144,7 @@ module Exec = struct -> new_alloc_num:Counter.t -> Dom.Mem.astate -> Dom.Mem.astate = - fun ~decl_sym_val array_kind pname symbol_table path tenv ~node_hash location ~depth loc typ + fun ~decl_sym_val deref_kind pname symbol_table path tenv ~node_hash location ~depth loc typ ?offset ?size ?stride ~inst_num ~new_sym_num ~new_alloc_num mem -> let option_value opt_x default_f = match opt_x with Some x -> x | None -> default_f () in let offset = @@ -156,7 +156,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 ~array_kind path in + let deref_path = Itv.SymbolPath.deref ~deref_kind path in let allocsite = let alloc_num = 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 312f276de..2e997cd99 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -68,7 +68,7 @@ module Exec : sig val decl_sym_arr : decl_sym_val:decl_sym_val - -> Symb.SymbolPath.c_sym_array_kind + -> Symb.SymbolPath.deref_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 d2ce71f8d..89136fe88 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/infer/src/bufferoverrun/symb.ml @@ -16,11 +16,11 @@ module BoundEnd = struct end module SymbolPath = struct - type c_sym_array_kind = CSymArray_Array | CSymArray_Pointer [@@deriving compare] + type deref_kind = Deref_ArrayIndex | Deref_CPointer [@@deriving compare] type partial = | Pvar of Pvar.t - | Index of c_sym_array_kind * partial + | Deref of deref_kind * partial | Field of Typ.Fieldname.t * partial [@@deriving compare] @@ -32,7 +32,7 @@ module SymbolPath = struct let field p fn = Field (fn, p) - let index ~array_kind p = Index (array_kind, p) + let deref ~deref_kind p = Deref (deref_kind, p) let normal p = Normal p @@ -43,7 +43,7 @@ module SymbolPath = struct let rec pp_partial fmt = function | Pvar pvar -> Pvar.pp_value fmt pvar - | Index (_, p) -> + | Deref (_, 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) @@ -61,9 +61,9 @@ module SymbolPath = struct let rec represents_multiple_values = function | Pvar _ -> false - | Index (CSymArray_Array, _) -> + | Deref (Deref_ArrayIndex, _) -> true - | Index (CSymArray_Pointer, p) + | Deref (Deref_CPointer, p) (* unsound but avoids many FPs for non-array pointers *) | Field (_, p) -> represents_multiple_values p diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index c9d176fd4..10f817dd9 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/infer/src/bufferoverrun/symb.mli @@ -15,11 +15,11 @@ module BoundEnd : sig end module SymbolPath : sig - type c_sym_array_kind = CSymArray_Array | CSymArray_Pointer [@@deriving compare] + type deref_kind = Deref_ArrayIndex | Deref_CPointer [@@deriving compare] type partial = private | Pvar of Pvar.t - | Index of c_sym_array_kind * partial + | Deref of deref_kind * partial | Field of Typ.Fieldname.t * partial [@@deriving compare] @@ -31,7 +31,7 @@ module SymbolPath : sig val of_pvar : Pvar.t -> partial - val index : array_kind:c_sym_array_kind -> partial -> partial + val deref : deref_kind:deref_kind -> partial -> partial val field : partial -> Typ.Fieldname.t -> partial