[inferbo] Distinguish unreachable and error status

Summary:
In Inferbo, the bottom memory is introduced when a node is unreachable by pruning, i.e.
`[[e]] <= [0,0]` on `prune(e)`.  This diff distinguishes whether `[[e]]` is `[0,0]` (unreachable)
or bottom (it could not evaluate `e` by some unknown reasons).

Reviewed By: ezgicicek

Differential Revision: D19902046

fbshipit-source-id: 7706017d6

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -72,7 +72,7 @@ module TransferFunctions = struct
         if Dom.LatestPrune.is_top latest_prune' then mem
         else Dom.Mem.set_latest_prune latest_prune' mem
     | Error `SubstBottom ->
-        Dom.Mem.bot
+        Dom.Mem.unreachable
     | Error `SubstFail ->
         mem
 
@@ -476,7 +476,7 @@ let compute_summary : (Pvar.t * Typ.t) list -> CFG.t -> invariant_map -> memory_
   | Some exit_mem ->
       exit_mem |> Dom.Mem.forget_unreachable_locs ~formals |> Dom.Mem.unset_oenv
   | None ->
-      Bottom
+      Unreachable
 
 
 let do_analysis : Callbacks.proc_callback_args -> Summary.t =

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -342,16 +342,16 @@ let check_instrs :
   match state with
   | _ when Instrs.is_empty instrs ->
       checks
-  | {AbstractInterpreter.State.pre= Dom.Mem.(Bottom | ExcRaised)} ->
+  | {AbstractInterpreter.State.pre= Dom.Mem.(Unreachable | Error | ExcRaised)} ->
       checks
-  | {AbstractInterpreter.State.pre= Dom.Mem.NonBottom _ as pre; post} ->
+  | {AbstractInterpreter.State.pre= Reachable _ as pre; post} ->
       if Instrs.nth_exists instrs 1 then L.(die InternalError) "Did not expect several instructions" ;
       let instr = Instrs.nth_exn instrs 0 in
       let checks =
         match post with
-        | Dom.Mem.(Bottom | ExcRaised) ->
+        | Dom.Mem.(Unreachable | ExcRaised) ->
             add_unreachable_code cfg node instr Instrs.empty checks
-        | Dom.Mem.NonBottom _ ->
+        | Dom.Mem.(Error | Reachable _) ->
             checks
       in
       let cond_set =

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -2333,13 +2333,15 @@ module MemReach = struct
 end
 
 module Mem = struct
-  type 'has_oenv t0 = Bottom | ExcRaised | NonBottom of 'has_oenv MemReach.t0
+  type 'has_oenv t0 = Unreachable | Error | ExcRaised | Reachable of 'has_oenv MemReach.t0
 
   type no_oenv_t = GOption.none t0
 
   type t = GOption.some t0
 
-  let bot : t = Bottom
+  let unreachable : t = Unreachable
+
+  let error : t = Error
 
   let exc_raised : t = ExcRaised
 
@@ -2349,15 +2351,19 @@ module Mem = struct
     if phys_equal lhs rhs then true
     else
       match (lhs, rhs) with
-      | Bottom, _ ->
+      | Unreachable, _ ->
+          true
+      | _, Unreachable ->
+          false
+      | Error, _ ->
           true
-      | _, Bottom ->
+      | _, Error ->
           false
       | ExcRaised, _ ->
           true
       | _, ExcRaised ->
           false
-      | NonBottom lhs, NonBottom rhs ->
+      | Reachable lhs, Reachable rhs ->
           MemReach.leq ~lhs ~rhs
 
 
@@ -2365,33 +2371,37 @@ module Mem = struct
     if phys_equal x y then x
     else
       match (x, y) with
-      | Bottom, m | m, Bottom ->
+      | Unreachable, m | m, Unreachable ->
+          m
+      | Error, m | m, Error ->
           m
       | ExcRaised, m | m, ExcRaised ->
           m
-      | NonBottom m1, NonBottom m2 ->
+      | Reachable m1, Reachable m2 ->
-          PhysEqual.optim2 ~res:(NonBottom (MemReach.join m1 m2)) x y
+          PhysEqual.optim2 ~res:(Reachable (MemReach.join m1 m2)) x y
 
 
   let widen ~prev:prev0 ~next:next0 ~num_iters =
     if phys_equal prev0 next0 then prev0
     else
       match (prev0, next0) with
-      | Bottom, m | m, Bottom ->
+      | Unreachable, m | m, Unreachable ->
+          m
+      | Error, m | m, Error ->
           m
       | ExcRaised, m | m, ExcRaised ->
           m
-      | NonBottom prev, NonBottom next ->
+      | Reachable prev, Reachable next ->
-          PhysEqual.optim2 ~res:(NonBottom (MemReach.widen ~prev ~next ~num_iters)) prev0 next0
+          PhysEqual.optim2 ~res:(Reachable (MemReach.widen ~prev ~next ~num_iters)) prev0 next0
 
 
   let map ~f x =
     match x with
-    | Bottom | ExcRaised ->
+    | Unreachable | Error | ExcRaised ->
         x
-    | NonBottom m ->
+    | Reachable m ->
         let m' = f m in
-        if phys_equal m' m then x else NonBottom m'
+        if phys_equal m' m then x else Reachable m'
 
 
   type get_summary = Procname.t -> no_oenv_t option
@@ -2399,13 +2409,14 @@ module Mem = struct
   let init : get_summary -> OndemandEnv.t -> t =
    fun get_summary oenv ->
     let get_summary pname =
-      match get_summary pname with Some (NonBottom m) -> Some m | _ -> None
+      match get_summary pname with Some (Reachable m) -> Some m | _ -> None
     in
-    NonBottom (MemReach.init get_summary oenv)
+    Reachable (MemReach.init get_summary oenv)
 
 
   let f_lift_default : default:'a -> ('h MemReach.t0 -> 'a) -> 'h t0 -> 'a =
-   fun ~default f m -> match m with Bottom | ExcRaised -> default | NonBottom m' -> f m'
+   fun ~default f m ->
+    match m with Unreachable | Error | ExcRaised -> default | Reachable m' -> f m'
 
 
   let is_stack_loc : Loc.t -> _ t0 -> bool =
@@ -2450,9 +2461,9 @@ module Mem = struct
   let find_ret_alias : _ t0 -> AliasTargets.t bottom_lifted =
    fun m ->
     match m with
-    | Bottom | ExcRaised ->
+    | Unreachable | Error | ExcRaised ->
         Bottom
-    | NonBottom m' ->
+    | Reachable m' ->
         NonBottom (MemReach.find_ret_alias m')
 
 
@@ -2503,8 +2514,8 @@ module Mem = struct
 
   let incr_iterator_simple_alias_on_call eval_sym_trace ~callee_exit_mem m =
     match (callee_exit_mem, m) with
-    | NonBottom callee_exit_mem, NonBottom m ->
+    | Reachable callee_exit_mem, Reachable m ->
-        NonBottom (MemReach.incr_iterator_simple_alias_on_call eval_sym_trace ~callee_exit_mem m)
+        Reachable (MemReach.incr_iterator_simple_alias_on_call eval_sym_trace ~callee_exit_mem m)
     | _, _ ->
         m
 
@@ -2556,11 +2567,11 @@ module Mem = struct
 
   let apply_latest_prune : Exp.t -> t -> t * PrunePairs.t =
    fun e -> function
-    | (Bottom | ExcRaised) as x ->
+    | (Unreachable | Error | ExcRaised) as x ->
         (x, PrunePairs.empty)
-    | NonBottom m ->
+    | Reachable m ->
         let m, prune_pairs = MemReach.apply_latest_prune e m in
-        (NonBottom m, prune_pairs)
+        (Reachable m, prune_pairs)
 
 
   let update_latest_prune : updated_locs:PowLoc.t -> Exp.t -> Exp.t -> t -> t =
@@ -2582,10 +2593,10 @@ module Mem = struct
   let forget_size_alias arr_locs = map ~f:(MemReach.forget_size_alias arr_locs)
 
   let unset_oenv = function
-    | (Bottom | ExcRaised) as x ->
+    | (Unreachable | Error | ExcRaised) as x ->
         x
-    | NonBottom m ->
+    | Reachable m ->
-        NonBottom (MemReach.unset_oenv m)
+        Reachable (MemReach.unset_oenv m)
 
 
   let set_first_idx_of_null loc idx = map ~f:(MemReach.set_first_idx_of_null loc idx)
@@ -2601,10 +2612,12 @@ module Mem = struct
 
   let pp f m =
     match m with
-    | Bottom ->
+    | Unreachable ->
-        F.pp_print_string f SpecialChars.up_tack
+        F.fprintf f "%s_unreachable" SpecialChars.up_tack
+    | Error ->
+        F.fprintf f "%s_our_fault" SpecialChars.up_tack
     | ExcRaised ->
         F.pp_print_string f (SpecialChars.up_tack ^ " by exception")
-    | NonBottom m ->
+    | Reachable m ->
         MemReach.pp f m
 end

infer/src/bufferoverrun/bufferOverrunDomain.mli

@@ -460,10 +460,13 @@ end
 
 module Mem : sig
   type 'has_oenv t0 =
-    | Bottom  (** Memory of unreachable node *)
+    | Unreachable  (** Memory of unreachable node *)
+    | Error
+        (** Error status due to Inferbo's incorrect semantics/models, e.g., when a value of an
+            abstract location is not found from the abstract memory inadvertently *)
     | ExcRaised
         (** Memory of node that can be reachable only with exception raises that we want to ignore *)
-    | NonBottom of 'has_oenv MemReach.t0
+    | Reachable of 'has_oenv MemReach.t0
 
   (** Memory type without an environment for on-demand symbol evaluation *)
   type no_oenv_t = GOption.none t0
@@ -477,7 +480,9 @@ module Mem : sig
 
   val pp : Format.formatter -> _ t0 -> unit
 
-  val bot : t
+  val unreachable : t
+
+  val error : t
 
   type get_summary = Procname.t -> no_oenv_t option
 

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -373,7 +373,7 @@ let by_risky_value_from lib_fun =
 
 
 let bottom =
-  let exec _model_env ~ret:_ _mem = Dom.Mem.bot in
+  let exec _model_env ~ret:_ _mem = Dom.Mem.unreachable in
   {exec; check= no_check}
 
 

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -748,17 +748,20 @@ module Prune = struct
         astate
 
 
-  let is_unreachable_constant : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> bool =
-   fun integer_type_widths e m ->
-    let v = eval integer_type_widths e m in
-    Itv.leq ~lhs:(Val.get_itv v) ~rhs:(Itv.of_int 0)
-    && PowLoc.is_bot (Val.get_pow_loc v)
-    && ArrayBlk.is_bot (Val.get_array_blk v)
-
-
   let prune_unreachable : Typ.IntegerWidths.t -> Exp.t -> t -> t =
    fun integer_type_widths e ({mem} as astate) ->
-    if is_unreachable_constant integer_type_widths e mem then {astate with mem= Mem.bot} else astate
+    match mem with
+    | Mem.(Unreachable | Error | ExcRaised) ->
+        astate
+    | Mem.Reachable _ ->
+        let v = eval integer_type_widths e mem in
+        let itv_v = Val.get_itv v in
+        if
+          Itv.leq ~lhs:itv_v ~rhs:(Itv.of_int 0)
+          && PowLoc.is_bot (Val.get_pow_loc v)
+          && ArrayBlk.is_bot (Val.get_array_blk v)
+        then {astate with mem= (if Itv.is_bottom itv_v then Mem.error else Mem.unreachable)}
+        else astate
 
 
   let rec prune_helper integer_type_widths e astate =
@@ -804,5 +807,6 @@ module Prune = struct
    fun integer_type_widths e mem ->
     let mem, prune_pairs = Mem.apply_latest_prune e mem in
     let {mem; prune_pairs} = prune_helper integer_type_widths e {mem; prune_pairs} in
-    if PrunePairs.is_reachable prune_pairs then Mem.set_prune_pairs prune_pairs mem else Mem.bot
+    if PrunePairs.is_reachable prune_pairs then Mem.set_prune_pairs prune_pairs mem
+    else Mem.unreachable
 end

infer/src/cost/boundMap.ml

@@ -55,15 +55,21 @@ let compute_upperbound_map node_cfg inferbo_invariant_map control_invariant_map
             (* bound = env(v1) *... * env(vn) *)
             let bound =
               match entry_mem with
-              | Bottom ->
+              | Unreachable ->
                   L.debug Analysis Medium
                     "@\n\
                      [COST ANALYSIS INTERNAL WARNING:] No 'env' found. This location is \
                      unreachable returning cost 0 \n" ;
                   BasicCost.zero
+              | Error ->
+                  L.debug Analysis Medium
+                    "@\n\
+                     [COST ANALYSIS INTERNAL WARNING:] No 'env' found. The Inferbo memory of this \
+                     location is erroneous \n" ;
+                  BasicCost.zero
               | ExcRaised ->
                   BasicCost.one
-              | NonBottom mem ->
+              | Reachable mem ->
                   let cost =
                     BufferOverrunDomain.MemReach.range ~filter_loc:(filter_loc control_map) ~node_id
                       mem