[inferbo] prune_eq_zero

Summary:
Convenience function for `prune_eq` with zero (needed for stacked diffs).
Renamed `prune_zero` to `prune_ne_zero` to avoid ambiguity.

Reviewed By: jvillard

Differential Revision: D7568556

fbshipit-source-id: b95ab6d

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -170,7 +170,9 @@ module Val = struct
     ; traces= TraceSet.join x.traces y.traces }
 
 
-  let prune_zero : t -> t = lift_prune1 Itv.prune_zero
+  let prune_eq_zero : t -> t = lift_prune1 Itv.prune_eq_zero
+
+  let prune_ne_zero : t -> t = lift_prune1 Itv.prune_ne_zero
 
   let prune_comp : Binop.t -> t -> t -> t =
    fun c -> lift_prune2 (Itv.prune_comp c) (ArrayBlk.prune_comp c)

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -355,12 +355,11 @@ module Prune = struct
       match Mem.find_alias x mem with
       | Some AliasTarget.Simple lv ->
           let v = Mem.find_heap lv mem in
-          let v' = Val.prune_zero v in
+          let v' = Val.prune_ne_zero v in
           update_mem_in_prune lv v' astate
       | Some AliasTarget.Empty lv ->
           let v = Mem.find_heap lv mem in
-          let itv_v = Itv.prune_eq (Val.get_itv v) Itv.zero in
-          let v' = Val.modify_itv itv_v v in
+          let v' = Val.prune_eq_zero v in
           update_mem_in_prune lv v' astate
       | None ->
           astate )
@@ -368,8 +367,7 @@ module Prune = struct
       match Mem.find_alias x mem with
       | Some AliasTarget.Simple lv ->
           let v = Mem.find_heap lv mem in
-          let itv_v = Itv.prune_eq (Val.get_itv v) Itv.false_sem in
-          let v' = Val.modify_itv itv_v v in
+          let v' = Val.prune_eq_zero v in
           update_mem_in_prune lv v' astate
       | Some AliasTarget.Empty lv ->
           let v = Mem.find_heap lv mem in

infer/src/bufferoverrun/itv.ml

@@ -1208,14 +1208,14 @@ module ItvPure = struct
 
   let prune_gt : t -> t -> t = fun x y -> prune_ge x (plus y one)
 
-  let diff : t -> Bound.t -> t =
+  let prune_diff : t -> Bound.t -> t =
    fun (l, u) b ->
     if Bound.eq l b then (Bound.plus_l l Bound.one, u)
     else if Bound.eq u b then (l, Bound.plus_u u Bound.mone)
     else (l, u)
 
 
-  let prune_zero : t -> t = fun x -> diff x Bound.zero
+  let prune_ne_zero : t -> t = fun x -> prune_diff x Bound.zero
 
   let prune_comp : Binop.t -> t -> t -> t option =
    fun c x y ->
@@ -1242,11 +1242,17 @@ module ItvPure = struct
     match prune_comp Binop.Le x y with None -> None | Some x' -> prune_comp Binop.Ge x' y
 
 
+  let prune_eq_zero : t -> t =
+   fun x ->
+    let x' = prune_le x zero in
+    prune_ge x' zero
+
+
   let prune_ne : t -> t -> t option =
    fun x (l, u) ->
     if is_invalid (l, u) then Some x
     else
-      let x = if Bound.eq l u then diff x l else x in
+      let x = if Bound.eq l u then prune_diff x l else x in
       if is_invalid x then None else Some x
 
 
@@ -1306,8 +1312,6 @@ let of_int64 : Int64.t -> astate =
 
 let is_false : t -> bool = function NonBottom x -> ItvPure.is_false x | Bottom -> false
 
-let false_sem = NonBottom ItvPure.false_sem
-
 let m1_255 = NonBottom ItvPure.m1_255
 
 let nat = NonBottom ItvPure.nat
@@ -1397,7 +1401,9 @@ let lor_sem : t -> t -> t = lift2 ItvPure.lor_sem
 
 let min_sem : t -> t -> t = lift2 ItvPure.min_sem
 
-let prune_zero : t -> t = lift1 ItvPure.prune_zero
+let prune_eq_zero : t -> t = lift1 ItvPure.prune_eq_zero
+
+let prune_ne_zero : t -> t = lift1 ItvPure.prune_ne_zero
 
 let prune_comp : Binop.t -> t -> t -> t = fun comp -> lift2_opt (ItvPure.prune_comp comp)
 

infer/src/bufferoverrun/itv.mli

@@ -143,9 +143,6 @@ type t = astate [@@deriving compare]
 val bot : t
 (** _|_ *)
 
-val false_sem : t
-(** 0 *)
-
 val m1_255 : t
 (** [-1, 255] *)
 
@@ -227,7 +224,9 @@ val mod_sem : t -> t -> t
 
 val ne_sem : t -> t -> t
 
-val prune_zero : t -> t
+val prune_eq_zero : t -> t
+
+val prune_ne_zero : t -> t
 
 val prune_comp : Binop.t -> t -> t -> t