From 0b26a57b8c2dd7c1d8eb670cbfadcb7075d25941 Mon Sep 17 00:00:00 2001
From: Sungkeun Cho <scho@fb.com>
Date: Tue, 3 Apr 2018 22:05:09 -0700
Subject: [PATCH] [inferbo] Revise semantics of plus and minus

Reviewed By: mbouaziz

Differential Revision: D7445018

fbshipit-source-id: 9083eab
---
 infer/src/bufferoverrun/bufferOverrunDomain.ml  | 17 ++++-------------
 infer/src/bufferoverrun/bufferOverrunModels.ml  |  2 +-
 .../src/bufferoverrun/bufferOverrunSemantics.ml |  4 ++--
 3 files changed, 7 insertions(+), 16 deletions(-)

diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index f99b814ee..d18386046 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/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 =
-   fun x y ->
-    { 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 plus_a : t -> t -> t =
+   fun x y -> {(lift_itv Itv.plus x y) with traces= TraceSet.join x.traces y.traces}
 
 
-  let minus : t -> t -> t =
-   fun x y ->
-    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 minus_a : t -> t -> t =
+   fun x y -> {(lift_itv Itv.minus x y) with traces= TraceSet.join x.traces y.traces}
 
 
   let mult : t -> t -> t =
diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml
index 4515a1d95..fc57ca8f7 100644
--- a/infer/src/bufferoverrun/bufferOverrunModels.ml
+++ b/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
diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
index 65e4c69dc..7725e7d08 100644
--- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml
+++ b/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 ->