[inferbo] Do not prune values with bottom

Summary: This diff avoids pruning values with bottom, which incorrectly introduced unreachable nodes.

Reviewed By: ezgicicek

Differential Revision: D20029764

fbshipit-source-id: 16ca2f196

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -635,6 +635,8 @@ module Val = struct
 
   let unknown_locs = of_pow_loc PowLoc.unknown ~traces:TraceSet.bottom
 
+  let is_bot x = Itv.is_bottom x.itv && PowLoc.is_bot x.powloc && ArrayBlk.is_bot x.arrayblk
+
   let is_mone x = Itv.is_mone (get_itv x)
 
   let is_incr_of l {itv} =
@@ -1564,10 +1566,7 @@ module CoreVal = struct
     if Itv.is_bottom itv then ArrayBlk.is_symbolic (Val.get_array_blk v) else Itv.is_symbolic itv
 
 
-  let is_empty v =
-    Itv.is_bottom (Val.get_itv v)
-    && PowLoc.is_empty (Val.get_pow_loc v)
-    && ArrayBlk.is_empty (Val.get_array_blk v)
+  let is_bot = Val.is_bot
 end
 
 module PruningExp = struct
@@ -1686,7 +1685,7 @@ module PrunedVal = struct
 
   let is_symbolic {v; pruning_exp} = CoreVal.is_symbolic v || PruningExp.is_symbolic pruning_exp
 
-  let is_empty {v; pruning_exp} = CoreVal.is_empty v || PruningExp.is_empty pruning_exp
+  let is_bot {v; pruning_exp} = CoreVal.is_bot v || PruningExp.is_empty pruning_exp
 end
 
 (* [PrunePairs] is a map from abstract locations to abstract values that represents pruned results
@@ -1713,7 +1712,7 @@ module PrunePairs = struct
     fold subst1 x (Ok empty)
 
 
-  let is_reachable x = not (exists (fun _ v -> PrunedVal.is_empty v) x)
+  let is_reachable x = not (exists (fun _ v -> PrunedVal.is_bot v) x)
 end
 
 module LatestPrune = struct
@@ -1923,7 +1922,7 @@ module Reachability = struct
     let exception Unreachable in
     let subst1 x acc =
       let v = PrunedVal.subst x eval_sym_trace location in
-      if PrunedVal.is_empty v then raise Unreachable else add v acc
+      if PrunedVal.is_bot v then raise Unreachable else add v acc
     in
     match M.fold subst1 x M.empty with x -> `Reachable x | exception Unreachable -> `Unreachable
 end

infer/src/bufferoverrun/bufferOverrunDomain.mli

@@ -108,6 +108,9 @@ module Val : sig
   val unknown_from : Typ.t -> callee_pname:Procname.t option -> location:Location.t -> t
   (** Unknown return value of [callee_pname] *)
 
+  val is_bot : t -> bool
+  (** Check if the value is bottom *)
+
   val is_mone : t -> bool
   (** Check if the value is [\[-1,-1\]] *)
 

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -655,9 +655,11 @@ module Prune = struct
             let v' = eval integer_type_widths e mem in
             if IntLit.iszero i then v' else Val.minus_a v' (Val.of_int_lit i)
           in
-          let v = val_prune_eq lhs rhs in
-          let pruning_exp = make_pruning_exp ~lhs ~rhs in
-          update_mem_in_prune lv v ~pruning_exp acc )
+          if Val.is_bot rhs then acc
+          else
+            let v = val_prune_eq lhs rhs in
+            let pruning_exp = make_pruning_exp ~lhs ~rhs in
+            update_mem_in_prune lv v ~pruning_exp acc )
     in
     gen_prune_alias_functions ~prune_alias_core
 

infer/tests/codetoanalyze/objc/performance/control.m

@@ -15,7 +15,7 @@ enum {
 };
 
 // expected linear
-bool wrong_cvar_FN(int x) {
+bool wrong_cvar_FP(int x) {
 
   while (true) {
     switch (x) {

infer/tests/codetoanalyze/objc/performance/issues.exp

@@ -2,7 +2,5 @@ codetoanalyze/objc/performance/cf.m, array_count_linear, 2, EXPENSIVE_EXECUTION_
 codetoanalyze/objc/performance/cf.m, cf_array_create_copy_linear, 6, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 1009, O(1), degree = 0]
 codetoanalyze/objc/performance/cf.m, cf_array_create_linear, 13, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 3 ⋅ x + 2 ⋅ (1+max(0, x)), O(x), degree = 1,{1+max(0, x)},Loop at line 41, column 3,{x},Loop at line 41, column 3]
 codetoanalyze/objc/performance/cf.m, dict_count_linear, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 3 ⋅ dict.length + 2 ⋅ (dict.length + 1), O(dict.length), degree = 1,{dict.length + 1},Loop at line 24, column 3,{dict.length},Loop at line 24, column 3]
-codetoanalyze/objc/performance/control.m, wrong_cvar_FN, 0, ZERO_EXECUTION_TIME, no_bucket, ERROR, []
-codetoanalyze/objc/performance/control.m, wrong_cvar_FN, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
-codetoanalyze/objc/performance/control.m, wrong_cvar_FN, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
-codetoanalyze/objc/performance/control.m, wrong_cvar_FN, 5, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
+codetoanalyze/objc/performance/control.m, wrong_cvar_FP, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 20, column 3]
+codetoanalyze/objc/performance/control.m, wrong_cvar_FP, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]