From da849cc320bc4cc53f9adf4bef2f22447176cb02 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 27 Nov 2019 10:15:56 -0800 Subject: [PATCH] [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 | 21 +++++++++++++++++++++ infer/src/bufferoverrun/itv.mli | 2 ++ infer/src/pulse/PulseAbductiveDomain.ml | 2 ++ infer/src/pulse/PulseAbductiveDomain.mli | 2 ++ infer/src/pulse/PulseAttribute.ml | 9 +++++++++ infer/src/pulse/PulseAttribute.mli | 2 ++ infer/src/pulse/PulseBaseMemory.ml | 8 ++++++++ infer/src/pulse/PulseBaseMemory.mli | 2 ++ infer/src/pulse/PulseOperations.ml | 18 +++++++++++------- 9 files changed, 59 insertions(+), 7 deletions(-) diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 16b61372d..2c32931d4 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/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 diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index c78038257..d9072d625 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/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 diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 28199fb81..a27eeee52 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/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) diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 36a576646..922650ad1 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/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 diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index 1adf0b6df..7a4c47171 100644 --- a/infer/src/pulse/PulseAttribute.ml +++ b/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 diff --git a/infer/src/pulse/PulseAttribute.mli b/infer/src/pulse/PulseAttribute.mli index 8474f8080..f81999942 100644 --- a/infer/src/pulse/PulseAttribute.mli +++ b/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 diff --git a/infer/src/pulse/PulseBaseMemory.ml b/infer/src/pulse/PulseBaseMemory.ml index 9b099838d..1c307e233 100644 --- a/infer/src/pulse/PulseBaseMemory.ml +++ b/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 diff --git a/infer/src/pulse/PulseBaseMemory.mli b/infer/src/pulse/PulseBaseMemory.mli index 902b8bfdb..55623429a 100644 --- a/infer/src/pulse/PulseBaseMemory.mli +++ b/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 diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 92743b48e..381a9bf1c 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -158,18 +158,18 @@ 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 - Option.both - (Memory.get_arithmetic addr_lhs astate) - (Memory.get_arithmetic addr_rhs astate) - |> Option.bind ~f:(function (a1, _), (a2, _) -> Arithmetic.binop bop a1 a2) - with + ( match + Option.both + (Memory.get_arithmetic addr_lhs astate) + (Memory.get_arithmetic addr_rhs astate) + |> Option.bind ~f:(function (a1, _), (a2, _) -> Arithmetic.binop bop a1 a2) + with | None -> (astate, (binop_addr, (* TODO history *) [])) | Some binop_a -> @@ -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