From 70fc1ab44a75eed5db5d08c3500bc60512821793 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 9 Dec 2019 09:16:37 -0800 Subject: [PATCH] [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 | 22 ++++++++------ infer/src/bufferoverrun/itv.mli | 2 ++ infer/src/pulse/PulseOperations.ml | 46 ++++++++++++++++++++---------- 3 files changed, 47 insertions(+), 23 deletions(-) diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 5ff7c9370..a5409705d 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/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 diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index d9072d625..63046423a 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/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 diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 118e56767..b5f959cce 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/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)) ->