From 82db1c13508791a7e2e629825c6c10e5ef7e17f7 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Fri, 29 Nov 2019 06:06:11 -0800 Subject: [PATCH] [pulse] Share subst function of itv Summary: This diff uses `Itv.subst` for substituting pulse's `BoItv` attributes. Reviewed By: jvillard Differential Revision: D18748308 fbshipit-source-id: bed7d4de8 --- infer/src/bufferoverrun/bounds.ml | 17 ------------ infer/src/bufferoverrun/bounds.mli | 5 ---- infer/src/bufferoverrun/itv.ml | 37 ++++--------------------- infer/src/bufferoverrun/itv.mli | 5 ---- infer/src/bufferoverrun/symb.ml | 24 +++++----------- infer/src/bufferoverrun/symb.mli | 5 +--- infer/src/pulse/PulseAbductiveDomain.ml | 30 ++++++++++++++------ 7 files changed, 35 insertions(+), 88 deletions(-) diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index 8a2a61fff..a1c9f96f4 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -209,14 +209,6 @@ module SymLinear = struct let exists_str ~f x = M.exists (fun k _ -> Symb.Symbol.exists_str ~f k) x - - let subst_pulse_value subst map = - M.fold - (fun symbol coeff (new_map, new_subst) -> - let new_subst, symbol' = Symb.Symbol.subst_pulse_value new_subst symbol in - let new_map = M.add symbol' coeff new_map in - (new_map, new_subst) ) - map (M.empty, subst) end module Bound = struct @@ -1145,15 +1137,6 @@ module Bound = struct let subst_ub x eval_sym = subst ~subst_pos:Symb.BoundEnd.UpperBound x eval_sym - let subst_pulse_value subst b = - match b with - | MInf | PInf | MinMax _ | MinMaxB _ -> - (subst, b) - | Linear (c, se) -> - let se', subst = SymLinear.subst_pulse_value subst se in - (subst, Linear (c, se')) - - (* When a positive bound is expected, min(1,x) can be simplified to 1. *) let simplify_min_one b = match b with diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli index 21a021477..1779b01fd 100644 --- a/infer/src/bufferoverrun/bounds.mli +++ b/infer/src/bufferoverrun/bounds.mli @@ -125,11 +125,6 @@ module Bound : sig val get_same_one_symbol : t -> t -> Symb.SymbolPath.t option val exists_str : f:(string -> bool) -> t -> bool - - val subst_pulse_value : - (PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t - -> t - -> (PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t * t end module BoundTrace : sig diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 4d36b2e53..5b84abf52 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -40,6 +40,10 @@ module ItvPure = struct let ub : t -> Bound.t = snd + let get_bound (lb, ub) bound_end = + match bound_end with Symb.BoundEnd.LowerBound -> lb | Symb.BoundEnd.UpperBound -> ub + + let is_lb_infty : t -> bool = fun (l, _) -> Bound.is_minf l let is_finite : t -> bool = @@ -394,16 +398,6 @@ module ItvPure = struct Bottom - let subst_pulse_values : - (PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t - -> t - -> (PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t * t = - fun subst (l, u) -> - let subst, l' = Bound.subst_pulse_value subst l in - let subst, u' = Bound.subst_pulse_value subst u in - (subst, (l', u')) - - let arith_binop bop x y = match bop with | Binop.PlusA _ -> @@ -549,14 +543,8 @@ let bot : t = Bottom let top : t = NonBottom ItvPure.top -let get_bound itv (be : Symb.BoundEnd.t) = - match (itv, be) with - | Bottom, _ -> - Bottom - | NonBottom x, LowerBound -> - NonBottom (ItvPure.lb x) - | NonBottom x, UpperBound -> - NonBottom (ItvPure.ub x) +let get_bound itv bound_end = + match itv with Bottom -> Bottom | NonBottom x -> NonBottom (ItvPure.get_bound x bound_end) let false_sem = NonBottom ItvPure.false_sem @@ -744,19 +732,6 @@ let subst : t -> Bound.eval_sym -> t = fun x eval_sym -> match x with NonBottom x' -> ItvPure.subst x' eval_sym | _ -> x -let subst_pulse_values : - (PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t - -> t - -> (PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t * t = - fun subst x -> - match x with - | NonBottom x' -> - let subst', x'' = ItvPure.subst_pulse_values subst x' in - (subst', NonBottom x'') - | Bottom -> - (subst, x) - - let is_symbolic = bind1bool ItvPure.is_symbolic let get_symbols : t -> SymbolSet.t = function diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 3f03939e2..d9072d625 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -243,11 +243,6 @@ val prune_le : t -> t -> t val subst : t -> Bound.eval_sym -> t -val subst_pulse_values : - (PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t - -> t - -> (PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t * t - val max_of_ikind : Typ.IntegerWidths.t -> Typ.ikind -> t val of_normal_path : unsigned:bool -> ?non_int:bool -> Symb.SymbolPath.partial -> t diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index a6b2166e6..25275f1af 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/infer/src/bufferoverrun/symb.ml @@ -366,6 +366,13 @@ module Symbol = struct false + let get_pulse_value_exn : t -> PulseAbstractValue.t = function + | PulseValue v -> + v + | OneValue _ | BoundEnd _ -> + assert false + + (* This should be called on non-pulse bound as of now. *) let path = function PulseValue _ -> assert false | OneValue {path} | BoundEnd {path} -> path @@ -387,23 +394,6 @@ module Symbol = struct false | OneValue {path} | BoundEnd {path} -> SymbolPath.exists_str ~f path - - - let subst_pulse_value subst s = - match s with - | OneValue _ | BoundEnd _ -> - (subst, s) - | PulseValue v -> - let subst', v' = - match PulseAbstractValue.Map.find_opt v subst with - | Some (v', _) -> - (subst, v') - | None -> - let v' = PulseAbstractValue.mk_fresh () in - let subst' = PulseAbstractValue.Map.add v (v', []) subst in - (subst', v') - in - (subst', PulseValue v') end module SymbolSet = struct diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index 6535449b0..8282bc9d0 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/infer/src/bufferoverrun/symb.mli @@ -124,10 +124,7 @@ module Symbol : sig val is_pulse_value : t -> bool - val subst_pulse_value : - (PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t - -> t - -> (PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t * t + val get_pulse_value_exn : t -> PulseAbstractValue.t end module SymbolSet : sig diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 4d860f326..3dc736d54 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -533,12 +533,23 @@ module PrePost = struct ~addr_pre ~addr_hist_caller call_state ) - let translate_attributes attrs_callee subst = - let translate_attribute subst attr = + let subst_attributes attrs_callee {astate; subst} = + let eval_sym_of_subst subst s bound_end = + let v = Symb.Symbol.get_pulse_value_exn s in + match PulseAbstractValue.Map.find_opt v !subst with + | Some (v', _) -> + Itv.get_bound (Memory.get_bo_itv v' astate) bound_end + | None -> + let v' = PulseAbstractValue.mk_fresh () in + subst := PulseAbstractValue.Map.add v (v', []) !subst ; + AbstractDomain.Types.NonBottom (Bounds.Bound.of_pulse_value v') + in + let subst_attribute subst attr = match (attr : Attribute.t) with | BoItv itv -> - let subst, itv' = Itv.subst_pulse_values subst itv in - (subst, Attribute.BoItv itv') + let subst = ref subst in + let itv' = Itv.subst itv (eval_sym_of_subst subst) in + (!subst, Attribute.BoItv itv') | AddressOfCppTemporary _ | AddressOfStackVariable _ | Arithmetic _ @@ -550,7 +561,7 @@ module PrePost = struct (* non-relational attributes *) (subst, attr) in - Attributes.fold_map attrs_callee ~init:subst ~f:translate_attribute + Attributes.fold_map attrs_callee ~init:subst ~f:subst_attribute let solve_arithmetic_constraints callee_proc_name call_location ~addr_pre ~attrs_pre @@ -592,7 +603,7 @@ module PrePost = struct let apply_arithmetic_constraints callee_proc_name call_location pre_post call_state = let one_address_sat addr_pre callee_attrs addr_hist_caller call_state = - let subst, attrs_pre = translate_attributes callee_attrs call_state.subst in + let subst, attrs_pre = subst_attributes callee_attrs call_state in solve_arithmetic_constraints callee_proc_name call_location ~addr_pre ~attrs_pre ~addr_hist_caller {call_state with subst} in @@ -681,7 +692,7 @@ module PrePost = struct | WrittenTo _ -> attr in - let call_state, attrs = translate_attributes attrs call_state in + let call_state, attrs = subst_attributes attrs call_state in (call_state, Attributes.map attrs ~f:(fun attr -> add_call_to_attribute attr)) @@ -693,7 +704,7 @@ module PrePost = struct let heap = (call_state.astate.post :> base_domain).heap in let subst, heap = let subst, attrs_post_caller = - add_call_to_attributes callee_proc_name call_loc hist_caller attrs_post call_state.subst + add_call_to_attributes callee_proc_name call_loc hist_caller attrs_post call_state in (subst, BaseMemory.set_attrs addr_caller attrs_post_caller heap) in @@ -863,7 +874,8 @@ module PrePost = struct (* callee address has no meaning for the caller *) (subst, heap) | Some (addr_caller, history) -> let subst, attrs' = - add_call_to_attributes callee_proc_name call_loc history attrs subst + add_call_to_attributes callee_proc_name call_loc history attrs + {call_state with subst} in (subst, BaseMemory.set_attrs addr_caller attrs' heap) ) (pre_post.post :> BaseDomain.t).heap (call_state.subst, heap0)