[inferbo] Ignore error memory status

Summary:
This ignores the error memory status (e.g. when condition expression is evaluated to bottom), in
order to keep analyze following code.

```
if ( e ) // e is evaluated to bottom due to a problem of Inferbo {
   ... // code here was not analyzed before
}
```

Reviewed By: ezgicicek

Differential Revision: D20067434

fbshipit-source-id: a1713722c

infer/src/bufferoverrun/bufferOverrunChecker.ml

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

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -2332,7 +2332,7 @@ module MemReach = struct
 end
 
 module Mem = struct
-  type 'has_oenv t0 = Unreachable | Error | ExcRaised | Reachable of 'has_oenv MemReach.t0
+  type 'has_oenv t0 = Unreachable | ExcRaised | Reachable of 'has_oenv MemReach.t0
 
   type no_oenv_t = GOption.none t0
 
@@ -2340,8 +2340,6 @@ module Mem = struct
 
   let unreachable : t = Unreachable
 
-  let error : t = Error
-
   let exc_raised : t = ExcRaised
 
   let is_exc_raised = function ExcRaised -> true | _ -> false
@@ -2354,10 +2352,6 @@ module Mem = struct
           true
       | _, Unreachable ->
           false
-      | Error, _ ->
-          true
-      | _, Error ->
-          false
       | ExcRaised, _ ->
           true
       | _, ExcRaised ->
@@ -2372,8 +2366,6 @@ module Mem = struct
       match (x, y) with
       | Unreachable, m | m, Unreachable ->
           m
-      | Error, m | m, Error ->
-          m
       | ExcRaised, m | m, ExcRaised ->
           m
       | Reachable m1, Reachable m2 ->
@@ -2386,8 +2378,6 @@ module Mem = struct
       match (prev0, next0) with
       | Unreachable, m | m, Unreachable ->
           m
-      | Error, m | m, Error ->
-          m
       | ExcRaised, m | m, ExcRaised ->
           m
       | Reachable prev, Reachable next ->
@@ -2396,7 +2386,7 @@ module Mem = struct
 
   let map ~f x =
     match x with
-    | Unreachable | Error | ExcRaised ->
+    | Unreachable | ExcRaised ->
         x
     | Reachable m ->
         let m' = f m in
@@ -2414,8 +2404,7 @@ module Mem = struct
 
 
   let f_lift_default : default:'a -> ('h MemReach.t0 -> 'a) -> 'h t0 -> 'a =
-   fun ~default f m ->
+   fun ~default f m -> match m with Unreachable | ExcRaised -> default | Reachable m' -> f m'
-    match m with Unreachable | Error | ExcRaised -> default | Reachable m' -> f m'
 
 
   let is_stack_loc : Loc.t -> _ t0 -> bool =
@@ -2460,7 +2449,7 @@ module Mem = struct
   let find_ret_alias : _ t0 -> AliasTargets.t bottom_lifted =
    fun m ->
     match m with
-    | Unreachable | Error | ExcRaised ->
+    | Unreachable | ExcRaised ->
         Bottom
     | Reachable m' ->
         NonBottom (MemReach.find_ret_alias m')
@@ -2566,7 +2555,7 @@ module Mem = struct
 
   let apply_latest_prune : Exp.t -> t -> t * PrunePairs.t =
    fun e -> function
-    | (Unreachable | Error | ExcRaised) as x ->
+    | (Unreachable | ExcRaised) as x ->
         (x, PrunePairs.empty)
     | Reachable m ->
         let m, prune_pairs = MemReach.apply_latest_prune e m in
@@ -2592,7 +2581,7 @@ module Mem = struct
   let forget_size_alias arr_locs = map ~f:(MemReach.forget_size_alias arr_locs)
 
   let unset_oenv = function
-    | (Unreachable | Error | ExcRaised) as x ->
+    | (Unreachable | ExcRaised) as x ->
         x
     | Reachable m ->
         Reachable (MemReach.unset_oenv m)
@@ -2613,8 +2602,6 @@ module Mem = struct
     match m with
     | Unreachable ->
         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")
     | Reachable m ->

infer/src/bufferoverrun/bufferOverrunDomain.mli

@@ -464,9 +464,6 @@ end
 module Mem : sig
   type 'has_oenv t0 =
     | 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 *)
     | Reachable of 'has_oenv MemReach.t0
@@ -485,8 +482,6 @@ module Mem : sig
 
   val unreachable : t
 
-  val error : t
-
   type get_summary = Procname.t -> no_oenv_t option
 
   val init : get_summary -> BufferOverrunOndemandEnv.t -> t

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -753,7 +753,7 @@ module Prune = struct
   let prune_unreachable : Typ.IntegerWidths.t -> Exp.t -> t -> t =
    fun integer_type_widths e ({mem} as astate) ->
     match mem with
-    | Mem.(Unreachable | Error | ExcRaised) ->
+    | Mem.(Unreachable | ExcRaised) ->
         astate
     | Mem.Reachable _ ->
         let v = eval integer_type_widths e mem in
@@ -762,7 +762,13 @@ module Prune = struct
           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)}
+        then
+          if Itv.is_bottom itv_v then
+            let () =
+              Logging.d_printfln_escaped "Warning: the condition expression is evaluated to bottom"
+            in
+            astate
+          else {astate with mem= Mem.unreachable}
         else astate
 
 

infer/src/cost/boundMap.ml

@@ -61,12 +61,6 @@ let compute_upperbound_map node_cfg inferbo_invariant_map control_invariant_map
                      [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
               | Reachable mem ->