[pulse] Add binop arithmetic for BoItv

Summary: This extends semantics of binary operator for BoItv. If there is no known interval value for a pulse value, it returns a symbolic value of the pulse value.

Reviewed By: jvillard

Differential Revision: D18726768

fbshipit-source-id: ed8ecf78b

infer/src/bufferoverrun/itv.ml

@@ -394,6 +394,16 @@ module ItvPure = struct
         Bottom
 
 
+  let arith_binop bop x y =
+    match bop with
+    | Binop.PlusA _ ->
+        Some (plus x y)
+    | Binop.MinusA _ ->
+        Some (minus x y)
+    | _ ->
+        None
+
+
   let prune_le : t -> t -> t = fun (l1, u1) (_, u2) -> (l1, Bound.overapprox_min u1 u2)
 
   let prune_ge : t -> t -> t = fun (l1, u1) (l2, _) -> (Bound.underapprox_max l1 l2, u1)
@@ -616,6 +626,15 @@ let lift2 : (ItvPure.t -> ItvPure.t -> ItvPure.t) -> t -> t -> t =
       NonBottom (f x y)
 
 
+let lift2opt : (ItvPure.t -> ItvPure.t -> ItvPure.t option) -> t -> t -> t option =
+ fun f x y ->
+  match (x, y) with
+  | Bottom, _ | _, Bottom ->
+      Some Bottom
+  | NonBottom x, NonBottom y ->
+      f x y |> Option.map ~f:(fun v -> NonBottom v)
+
+
 let bind2_gen : bot:'a -> (ItvPure.t -> ItvPure.t -> 'a) -> t -> t -> 'a =
  fun ~bot f x y ->
   match (x, y) with Bottom, _ | _, Bottom -> bot | NonBottom x, NonBottom y -> f x y
@@ -693,6 +712,8 @@ let max_sem : ?use_minmax_bound:bool -> t -> t -> t =
  fun ?use_minmax_bound -> lift2 (ItvPure.max_sem ?use_minmax_bound)
 
 
+let arith_binop : Binop.t -> t -> t -> t option = fun bop -> lift2opt (ItvPure.arith_binop bop)
+
 let prune_eq_zero : t -> t = bind1 ItvPure.prune_eq_zero
 
 let prune_ne_zero : t -> t = bind1 ItvPure.prune_ne_zero

infer/src/bufferoverrun/itv.mli

@@ -223,6 +223,8 @@ val mod_sem : t -> t -> t
 
 val ne_sem : t -> t -> Boolean.t
 
+val arith_binop : Binop.t -> t -> t -> t option
+
 val prune_eq_zero : t -> t
 
 val prune_ne_zero : t -> t

infer/src/pulse/PulseAbductiveDomain.ml

@@ -215,6 +215,8 @@ module Memory = struct
 
   let get_arithmetic addr astate = BaseMemory.get_arithmetic addr (astate.post :> base_domain).heap
 
+  let get_bo_itv addr astate = BaseMemory.get_bo_itv addr (astate.post :> base_domain).heap
+
   let std_vector_reserve addr astate =
     map_post_heap astate ~f:(fun heap -> BaseMemory.std_vector_reserve addr heap)
 

infer/src/pulse/PulseAbductiveDomain.mli

@@ -81,6 +81,8 @@ module Memory : sig
       returns what it points to or creates a fresh value if that edge didn't exist.  *)
 
   val get_arithmetic : AbstractValue.t -> t -> (Arithmetic.t * Trace.t) option
+
+  val get_bo_itv : AbstractValue.t -> t -> Itv.t
 end
 
 val is_local : Var.t -> t -> bool

infer/src/pulse/PulseAttribute.ml

@@ -65,6 +65,8 @@ module Attribute = struct
 
   let const_rank = Variants.to_rank (Arithmetic (Arithmetic.equal_to IntLit.zero, dummy_trace))
 
+  let bo_itv_rank = Variants.to_rank (BoItv Itv.zero)
+
   let pp f attribute =
     let pp_string_if_debug string fmt =
       if Config.debug_level_analysis >= 3 then F.pp_print_string fmt string
@@ -146,6 +148,13 @@ module Attributes = struct
            (a, trace) )
 
 
+  let get_bo_itv attrs =
+    Set.find_rank attrs Attribute.bo_itv_rank
+    |> Option.map ~f:(fun attr ->
+           let[@warning "-8"] (Attribute.BoItv itv) = attr in
+           itv )
+
+
   include Set
 end
 

infer/src/pulse/PulseAttribute.mli

@@ -34,6 +34,8 @@ module Attributes : sig
 
   val get_arithmetic : t -> (Arithmetic.t * Trace.t) option
 
+  val get_bo_itv : t -> Itv.t option
+
   val get_invalid : t -> (Invalidation.t * Trace.t) option
 
   val get_must_be_valid : t -> Trace.t option

infer/src/pulse/PulseBaseMemory.ml

@@ -90,6 +90,14 @@ let get_closure_proc_name = get_attribute Attributes.get_closure_proc_name
 
 let get_arithmetic = get_attribute Attributes.get_arithmetic
 
+let get_bo_itv v memory =
+  match get_attribute Attributes.get_bo_itv v memory with
+  | None ->
+      Itv.of_pulse_value v
+  | Some itv ->
+      itv
+
+
 let get_must_be_valid = get_attribute Attributes.get_must_be_valid
 
 let std_vector_reserve address memory = add_attribute address Attribute.StdVectorReserve memory

infer/src/pulse/PulseBaseMemory.mli

@@ -62,6 +62,8 @@ val get_closure_proc_name : AbstractValue.t -> t -> Typ.Procname.t option
 
 val get_arithmetic : AbstractValue.t -> t -> (Arithmetic.t * Trace.t) option
 
+val get_bo_itv : AbstractValue.t -> t -> Itv.t
+
 val get_must_be_valid : AbstractValue.t -> t -> Trace.t option
 
 val std_vector_reserve : AbstractValue.t -> t -> t

infer/src/pulse/PulseOperations.ml

@@ -158,13 +158,13 @@ let eval location exp0 astate =
             let unop_trace = Trace.Immediate {location; history= unop_hist} in
             let astate = Memory.add_attribute unop_addr (Arithmetic (unop_a, unop_trace)) astate in
             (astate, (unop_addr, unop_hist)) )
-    | BinOp (bop, e_lhs, e_rhs) -> (
+    | BinOp (bop, e_lhs, e_rhs) ->
         eval e_lhs astate
         >>= fun (astate, (addr_lhs, hist_lhs)) ->
         eval e_rhs astate
         >>| fun (astate, (addr_rhs, _hist_rhs)) ->
         let binop_addr = AbstractValue.mk_fresh () in
-        match
+        ( match
             Option.both
               (Memory.get_arithmetic addr_lhs astate)
               (Memory.get_arithmetic addr_rhs astate)
@@ -179,6 +179,10 @@ let eval location exp0 astate =
               Memory.add_attribute binop_addr (Arithmetic (binop_a, binop_trace)) astate
             in
             (astate, (binop_addr, binop_hist)) )
+        |> fun ((astate, ((addr, _) as addr_hist)) as default) ->
+        Itv.arith_binop bop (Memory.get_bo_itv addr_lhs astate) (Memory.get_bo_itv addr_rhs astate)
+        |> Option.value_map ~default ~f:(fun itv ->
+               (Memory.add_attribute addr (BoItv itv) astate, addr_hist) )
     | Const _ | Sizeof _ | Exn _ ->
         Ok (astate, (AbstractValue.mk_fresh (), (* TODO history *) []))
   in