[pulse] eval unops using inferbo

Summary:
Similarly to binops, let inferbo evaluate unary operations and record
the results.

Reviewed By: ezgicicek

Differential Revision: D18811146

fbshipit-source-id: 8f9e16bbd

infer/src/bufferoverrun/itv.ml

@@ -402,15 +402,11 @@ 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 arith_binop (bop : Binop.t) x y =
+    match bop with PlusA _ -> Some (plus x y) | MinusA _ -> Some (minus x y) | _ -> None
+
 
+  let arith_unop (unop : Unop.t) x = match unop with Neg -> Some (neg x) | BNot | LNot -> None
 
   let prune_le : t -> t -> t = fun (l1, u1) (_, u2) -> (l1, Bound.overapprox_min u1 u2)
 
@@ -607,6 +603,14 @@ let lift1 : (ItvPure.t -> ItvPure.t) -> t -> t =
  fun f -> function Bottom -> Bottom | NonBottom x -> NonBottom (f x)
 
 
+let lift1opt : (ItvPure.t -> ItvPure.t option) -> t -> t option =
+ fun f -> function
+  | Bottom ->
+      Some Bottom
+  | NonBottom x ->
+      f x |> Option.map ~f:(fun v -> NonBottom v)
+
+
 let bind1_gen : bot:'a -> (ItvPure.t -> 'a) -> t -> 'a =
  fun ~bot f x -> match x with Bottom -> bot | NonBottom x -> f x
 
@@ -716,6 +720,8 @@ let max_sem : ?use_minmax_bound:bool -> t -> t -> t =
 
 let arith_binop : Binop.t -> t -> t -> t option = fun bop -> lift2opt (ItvPure.arith_binop bop)
 
+let arith_unop : Unop.t -> t -> t option = fun unop -> lift1opt (ItvPure.arith_unop unop)
+
 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

@@ -225,6 +225,8 @@ val ne_sem : t -> t -> Boolean.t
 
 val arith_binop : Binop.t -> t -> t -> t option
 
+val arith_unop : Unop.t -> t -> t option
+
 val prune_eq_zero : t -> t
 
 val prune_ne_zero : t -> t

infer/src/pulse/PulseOperations.ml

@@ -142,6 +142,35 @@ let eval_binop location binop op_lhs op_rhs binop_hist astate =
   (astate, (binop_addr, binop_hist))
 
 
+let eval_unop_arith location unop_addr unop operand_addr unop_hist astate =
+  match
+    Memory.get_arithmetic operand_addr astate
+    |> Option.bind ~f:(function a, _ -> Arithmetic.unop unop a)
+  with
+  | None ->
+      astate
+  | Some unop_a ->
+      let unop_trace = Trace.Immediate {location; history= unop_hist} in
+      Memory.add_attribute unop_addr (Arithmetic (unop_a, unop_trace)) astate
+
+
+let eval_unop_bo_itv unop_addr unop operand_addr astate =
+  match Itv.arith_unop unop (Memory.get_bo_itv operand_addr astate) with
+  | None ->
+      astate
+  | Some itv ->
+      Memory.add_attribute unop_addr (BoItv itv) astate
+
+
+let eval_unop location unop addr unop_hist astate =
+  let unop_addr = AbstractValue.mk_fresh () in
+  let astate =
+    eval_unop_arith location unop_addr unop addr unop_hist astate
+    |> eval_unop_bo_itv unop_addr unop addr
+  in
+  (astate, (unop_addr, unop_hist))
+
+
 let eval location exp0 astate =
   let rec eval exp astate =
     match (exp : Exp.t) with
@@ -189,21 +218,8 @@ let eval location exp0 astate =
                (ConstantDereference i) location
         in
         Ok (astate, (addr, []))
-    | UnOp (unop, exp, _typ) -> (
-        eval exp astate
-        >>| fun (astate, (addr, hist)) ->
-        let unop_addr = AbstractValue.mk_fresh () in
-        match
-          Memory.get_arithmetic addr astate
-          |> Option.bind ~f:(function a, _ -> Arithmetic.unop unop a)
-        with
-        | None ->
-            (astate, (unop_addr, (* TODO history *) []))
-        | Some unop_a ->
-            let unop_hist = (* TODO: add event *) hist in
-            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)) )
+    | UnOp (unop, exp, _typ) ->
+        eval exp astate >>| fun (astate, (addr, hist)) -> eval_unop location unop addr hist astate
     | BinOp (bop, e_lhs, e_rhs) ->
         eval e_lhs astate
         >>= fun (astate, (addr_lhs, hist_lhs)) ->