[inferbo] Precise unknown value depending on type

Summary:
This diff revises the generation of unknown value. If the type of the unknown value generating is
int, it does not add the "Unknown" pointer/array value.

Reviewed By: ngorogiannis

Differential Revision: D19392696

fbshipit-source-id: e1b3c9a3a

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -274,7 +274,7 @@ module TransferFunctions = struct
         None
 
 
-  let load_global_constant get_summary id pvar location mem ~find_from_initializer =
+  let load_global_constant get_summary ((id, _) as ret) pvar location mem ~find_from_initializer =
     match Pvar.get_initializer_pname pvar with
     | Some callee_pname -> (
       match get_summary callee_pname with
@@ -284,11 +284,11 @@ module TransferFunctions = struct
       | None ->
           L.d_printfln_escaped "/!\\ Unknown initializer of global constant %a" (Pvar.pp Pp.text)
             pvar ;
-          Dom.Mem.add_unknown_from id ~callee_pname ~location mem )
+          Dom.Mem.add_unknown_from ret ~callee_pname ~location mem )
     | None ->
         L.d_printfln_escaped "/!\\ Failed to get initializer name of global constant %a"
           (Pvar.pp Pp.text) pvar ;
-        Dom.Mem.add_unknown id ~location mem
+        Dom.Mem.add_unknown ret ~location mem
 
 
   let exec_instr : Dom.Mem.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.t =
@@ -297,13 +297,13 @@ module TransferFunctions = struct
     match instr with
     | Load {id} when Ident.is_none id ->
         mem
-    | Load {id; e= Exp.Lvar pvar; loc= location}
+    | Load {id; e= Exp.Lvar pvar; typ; loc= location}
       when Pvar.is_compile_constant pvar || Pvar.is_ice pvar ->
-        load_global_constant get_summary id pvar location mem
+        load_global_constant get_summary (id, typ) pvar location mem
           ~find_from_initializer:(fun callee_mem -> Dom.Mem.find (Loc.of_pvar pvar) callee_mem)
-    | Load {id; e= Exp.Lindex (Exp.Lvar pvar, _); loc= location}
+    | Load {id; e= Exp.Lindex (Exp.Lvar pvar, _); typ; loc= location}
       when Pvar.is_compile_constant pvar || Pvar.is_ice pvar ->
-        load_global_constant get_summary id pvar location mem
+        load_global_constant get_summary (id, typ) pvar location mem
           ~find_from_initializer:(fun callee_mem ->
             let locs = Dom.Mem.find (Loc.of_pvar pvar) callee_mem |> Dom.Val.get_all_locs in
             Dom.Mem.find_set locs callee_mem )
@@ -408,11 +408,11 @@ module TransferFunctions = struct
                   L.(debug BufferOverrun Verbose)
                     "/!\\ Non-static call to unknown %a \n\n" Procname.pp callee_pname ;
                   assign_symbolic_pname_value callee_pname params ret location mem )
-                else Dom.Mem.add_unknown_from id ~callee_pname ~location mem ) )
-    | Call ((id, _), fun_exp, _, location, _) ->
+                else Dom.Mem.add_unknown_from ret ~callee_pname ~location mem ) )
+    | Call (((id, _) as ret), fun_exp, _, location, _) ->
         let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in
         L.d_printfln_escaped "/!\\ Call to non-const function %a" Exp.pp fun_exp ;
-        Dom.Mem.add_unknown id ~location mem
+        Dom.Mem.add_unknown ret ~location mem
     | Metadata (VariableLifetimeBegins (pvar, typ, location)) when Pvar.is_global pvar ->
         let model_env =
           let pname = Summary.get_proc_name summary in

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -126,15 +126,16 @@ module Val = struct
       ArrayBlk.pp x.arrayblk trace_pp x.traces
 
 
-  let unknown_from : callee_pname:_ -> location:_ -> t =
-   fun ~callee_pname ~location ->
+  let unknown_from : Typ.t -> callee_pname:_ -> location:_ -> t =
+   fun typ ~callee_pname ~location ->
+    let is_int = Typ.is_int typ in
     let traces = Trace.(Set.singleton_final location (UnknownFrom callee_pname)) in
     { itv= Itv.top
     ; itv_thresholds= ItvThresholds.empty
     ; itv_updated_by= ItvUpdatedBy.Top
     ; modeled_range= ModeledRange.bottom
-    ; powloc= PowLoc.unknown
-    ; arrayblk= ArrayBlk.unknown
+    ; powloc= (if is_int then PowLoc.bottom else PowLoc.unknown)
+    ; arrayblk= (if is_int then ArrayBlk.bottom else ArrayBlk.unknown)
     ; traces }
 
 
@@ -1984,10 +1985,10 @@ module MemReach = struct
     PowLoc.fold (fun l acc -> add_heap ?represents_multiple_values l v acc) locs m
 
 
-  let add_unknown_from : Ident.t -> callee_pname:Procname.t option -> location:Location.t -> t -> t
-      =
-   fun id ~callee_pname ~location m ->
-    let val_unknown = Val.unknown_from ~callee_pname ~location in
+  let add_unknown_from :
+      Ident.t * Typ.t -> callee_pname:Procname.t option -> location:Location.t -> t -> t =
+   fun (id, typ) ~callee_pname ~location m ->
+    let val_unknown = Val.unknown_from typ ~callee_pname ~location in
     add_stack (Loc.of_id id) val_unknown m |> add_heap Loc.unknown val_unknown
 
 
@@ -2356,13 +2357,14 @@ module Mem = struct
     map ~f:(MemReach.add_heap_set ?represents_multiple_values ploc v)
 
 
-  let add_unknown_from : Ident.t -> callee_pname:Procname.t -> location:Location.t -> t -> t =
-   fun id ~callee_pname ~location ->
-    map ~f:(MemReach.add_unknown_from id ~callee_pname:(Some callee_pname) ~location)
+  let add_unknown_from : Ident.t * Typ.t -> callee_pname:Procname.t -> location:Location.t -> t -> t
+      =
+   fun ret ~callee_pname ~location ->
+    map ~f:(MemReach.add_unknown_from ret ~callee_pname:(Some callee_pname) ~location)
 
 
-  let add_unknown : Ident.t -> location:Location.t -> t -> t =
-   fun id ~location -> map ~f:(MemReach.add_unknown_from id ~callee_pname:None ~location)
+  let add_unknown : Ident.t * Typ.t -> location:Location.t -> t -> t =
+   fun ret ~location -> map ~f:(MemReach.add_unknown_from ret ~callee_pname:None ~location)
 
 
   let strong_update : PowLoc.t -> Val.t -> t -> t = fun p v -> map ~f:(MemReach.strong_update p v)

infer/src/bufferoverrun/bufferOverrunDomain.mli

@@ -83,7 +83,7 @@ module Val : sig
 
   val unknown_locs : t
 
-  val unknown_from : callee_pname:Procname.t option -> location:Location.t -> t
+  val unknown_from : Typ.t -> callee_pname:Procname.t option -> location:Location.t -> t
   (** Unknown return value of [callee_pname] *)
 
   val is_mone : t -> bool
@@ -502,10 +502,10 @@ module Mem : sig
 
   val add_heap_set : ?represents_multiple_values:bool -> AbsLoc.PowLoc.t -> Val.t -> t -> t
 
-  val add_unknown : Ident.t -> location:Location.t -> t -> t
+  val add_unknown : Ident.t * Typ.t -> location:Location.t -> t -> t
   (** Add an unknown value for stack variables *)
 
-  val add_unknown_from : Ident.t -> callee_pname:Procname.t -> location:Location.t -> t -> t
+  val add_unknown_from : Ident.t * Typ.t -> callee_pname:Procname.t -> location:Location.t -> t -> t
   (** Add an unknown return value of [callee_pname] for stack variables *)
 
   val remove_temps : Ident.t list -> t -> t

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -26,9 +26,9 @@ type model = {exec: exec_fun; check: check_fun}
 let no_check _model_env _mem cond_set = cond_set
 
 let no_model =
-  let exec {pname; location} ~ret:(id, _) mem =
+  let exec {pname; location} ~ret mem =
     L.d_printfln_escaped "No model for %a" Procname.pp pname ;
-    Dom.Mem.add_unknown_from id ~callee_pname:pname ~location mem
+    Dom.Mem.add_unknown_from ret ~callee_pname:pname ~location mem
   in
   {exec; check= no_check}
 
@@ -565,10 +565,10 @@ module ArrObjCommon = struct
 
 
   let at arr_exp ~fn index_exp =
-    let exec ({pname; location} as model_env) ~ret:(id, _) mem =
+    let exec ({pname; location} as model_env) ~ret:(id, typ) mem =
       let array_v =
         let locs = deref_of model_env arr_exp ~fn mem in
-        if PowLoc.is_bot locs then Dom.Val.unknown_from ~callee_pname:(Some pname) ~location
+        if PowLoc.is_bot locs then Dom.Val.unknown_from typ ~callee_pname:(Some pname) ~location
         else Dom.Mem.find_set locs mem
       in
       Dom.Mem.add_stack (Loc.of_id id) array_v mem