[inferbo] Revise semantics of plus and minus

Reviewed By: mbouaziz

Differential Revision: D7445018

fbshipit-source-id: 9083eab

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -80,8 +80,6 @@ module Val = struct
       ; traces= TraceSet.join x.traces y.traces }
 
 
-  let rec joins : t list -> t = function [] -> bot | [a] -> a | a :: b -> join a (joins b)
-
   let get_itv : t -> Itv.t = fun x -> x.itv
 
   let get_pow_loc : t -> PowLoc.t = fun x -> x.powloc
@@ -128,19 +126,12 @@ module Val = struct
     if has_pointer x || has_pointer y then {bot with itv= Itv.unknown_bool} else lift_itv f x y
 
 
-  let plus : t -> t -> t =
+  let plus_a : t -> t -> t =
-   fun x y ->
+   fun x y -> {(lift_itv Itv.plus x y) with traces= TraceSet.join x.traces y.traces}
-    { x with
-      itv= Itv.plus x.itv y.itv
-    ; arrayblk= ArrayBlk.plus_offset x.arrayblk y.itv
-    ; traces= TraceSet.join x.traces y.traces }
 
 
-  let minus : t -> t -> t =
+  let minus_a : t -> t -> t =
-   fun x y ->
+   fun x y -> {(lift_itv Itv.minus x y) with traces= TraceSet.join x.traces y.traces}
-    let n = Itv.join (Itv.minus x.itv y.itv) (ArrayBlk.diff x.arrayblk y.arrayblk) in
-    let a = ArrayBlk.minus_offset x.arrayblk y.itv in
-    {bot with itv= n; arrayblk= a; traces= TraceSet.join x.traces y.traces}
 
 
   let mult : t -> t -> t =

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -223,7 +223,7 @@ module Split = struct
     let vector_size_locs =
       Sem.eval vector_exp mem |> Dom.Val.get_all_locs |> PowLoc.append_field ~fn:size_field
     in
-    Dom.Mem.transform_mem ~f:(Dom.Val.plus increment) vector_size_locs mem
+    Dom.Mem.transform_mem ~f:(Dom.Val.plus_a increment) vector_size_locs mem
 end
 
 module Boost = struct

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -251,11 +251,11 @@ and eval_binop : Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Val.t =
   let v2 = eval e2 mem in
   match binop with
   | Binop.PlusA ->
-      Val.join (Val.plus v1 v2) (Val.plus_pi v1 v2)
+      Val.plus_a v1 v2
   | Binop.PlusPI ->
       Val.plus_pi v1 v2
   | Binop.MinusA ->
-      Val.joins [Val.minus v1 v2; Val.minus_pi v1 v2; Val.minus_pp v1 v2]
+      Val.minus_a v1 v2
   | Binop.MinusPI ->
       Val.minus_pi v1 v2
   | Binop.MinusPP ->