[Inferbo] Differentiate array and pointer in SymbolPaths

Reviewed By: jvillard

Differential Revision: D12939124

fbshipit-source-id: 256d0b159

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 -> (

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}
 

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) ->

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)

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

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)

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