From 9610ceb4b84661fa0713a7f14a951950bab76a05 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 29 Nov 2019 03:15:56 -0800 Subject: [PATCH] [pulse] substitute inferbo attributes in callee summaries Summary: The introduction of inferbo intervals as pulse attributes creates the first relational attributes. To make sense of inferbo intervals appearing in summaries when in a caller context, we need to substitute the abstract values they contain in the callee with the abstract values they correspond to in the caller. This has a significant consequence: we have to delay the check that arithmetic constraints in the callee are satisfiable at the call-site until *after* we have discovered all the relationships between callee values and caller values from the heap. To solve this, we now run an arithmetic constraints check *after* having materialised all the addresses. We also need to translate the abstract values in the attributes in the post before recording them in the caller, for the same reasons. Quite some code in this diff is concerned with substituting pulse values inside inferbo intervals. There is a complication there too: even after having discovered relationships between caller and callee abstract values induced by the heap shapes, there could be abstract values in the callee's attributes that we haven't seen yet. We need to make up new values for these in the caller, so this substitution has to return a potentially extended substitution. Reviewed By: skcho Differential Revision: D18745695 fbshipit-source-id: 077ae7670 --- infer/src/bufferoverrun/bounds.ml | 17 ++ infer/src/bufferoverrun/bounds.mli | 5 + infer/src/bufferoverrun/itv.ml | 23 +++ infer/src/bufferoverrun/itv.mli | 5 + infer/src/bufferoverrun/symb.ml | 24 +++ infer/src/bufferoverrun/symb.mli | 7 + infer/src/istd/PrettyPrintable.ml | 13 ++ infer/src/istd/PrettyPrintable.mli | 2 + infer/src/pulse/PulseAbductiveDomain.ml | 200 ++++++++++++++---------- 9 files changed, 214 insertions(+), 82 deletions(-) diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index a1c9f96f4..8a2a61fff 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -209,6 +209,14 @@ 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 @@ -1137,6 +1145,15 @@ 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 1779b01fd..21a021477 100644 --- a/infer/src/bufferoverrun/bounds.mli +++ b/infer/src/bufferoverrun/bounds.mli @@ -125,6 +125,11 @@ 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 2c32931d4..4d36b2e53 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -394,6 +394,16 @@ 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 _ -> @@ -734,6 +744,19 @@ 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 d9072d625..3f03939e2 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -243,6 +243,11 @@ 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 37c2f3b9c..a6b2166e6 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/infer/src/bufferoverrun/symb.ml @@ -359,6 +359,13 @@ module Symbol = struct SymbolPath.is_global path + let is_pulse_value : t -> bool = function + | PulseValue _ -> + true + | OneValue _ | BoundEnd _ -> + false + + (* This should be called on non-pulse bound as of now. *) let path = function PulseValue _ -> assert false | OneValue {path} | BoundEnd {path} -> path @@ -380,6 +387,23 @@ 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 ff2cd7c7a..6535449b0 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/infer/src/bufferoverrun/symb.mli @@ -121,6 +121,13 @@ module Symbol : sig val of_pulse_value : PulseAbstractValue.t -> t val exists_str : f:(string -> bool) -> t -> bool + + 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 end module SymbolSet : sig diff --git a/infer/src/istd/PrettyPrintable.ml b/infer/src/istd/PrettyPrintable.ml index 34836040e..41e1d9cf0 100644 --- a/infer/src/istd/PrettyPrintable.ml +++ b/infer/src/istd/PrettyPrintable.ml @@ -221,6 +221,8 @@ module type PPUniqRankSet = sig val fold : t -> init:'accum -> f:('accum -> elt -> 'accum) -> 'accum + val fold_map : t -> init:'accum -> f:('accum -> elt -> 'accum * elt) -> 'accum * t + val is_empty : t -> bool val is_singleton : t -> bool @@ -273,6 +275,17 @@ module MakePPUniqRankSet (Val : PrintableRankedType) : PPUniqRankSet with type e m + let fold_map m ~init ~f = + let accum = ref init in + let m' = + map m ~f:(fun value -> + let acc', v' = f !accum value in + accum := acc' ; + v' ) + in + (!accum, m') + + let pp ?(print_rank = false) fmt map = if print_rank then Map.pp fmt map else pp_collection ~pp_item:Val.pp fmt (Map.bindings map |> List.map ~f:snd) diff --git a/infer/src/istd/PrettyPrintable.mli b/infer/src/istd/PrettyPrintable.mli index cba82e0c4..f2e302d08 100644 --- a/infer/src/istd/PrettyPrintable.mli +++ b/infer/src/istd/PrettyPrintable.mli @@ -172,6 +172,8 @@ module type PPUniqRankSet = sig val fold : t -> init:'accum -> f:('accum -> elt -> 'accum) -> 'accum + val fold_map : t -> init:'accum -> f:('accum -> elt -> 'accum * elt) -> 'accum * t + val is_empty : t -> bool val is_singleton : t -> bool diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index a27eeee52..4d860f326 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -446,43 +446,6 @@ module PrePost = struct Trace.ViaCall {f= Call proc_name; location= call_location; history= caller_history; in_call} - let solve_arithmetic_constraints callee_proc_name call_location ~addr_pre ~attrs_pre - ~addr_hist_caller call_state = - match Attributes.get_arithmetic attrs_pre with - | None -> - call_state - | Some (arith_callee, arith_callee_hist) -> ( - let addr_caller, hist_caller = addr_hist_caller in - let astate = call_state.astate in - let arith_caller_opt = Memory.get_arithmetic addr_caller astate |> Option.map ~f:fst in - (* TODO: we don't use [abduced_callee] but we could probably use it to refine the attributes - for that address in the post since abstract values are immutable *) - match - Arithmetic.abduce_binop_is_true ~negated:false Eq arith_caller_opt (Some arith_callee) - with - | Unsatisfiable -> - raise - (CannotApplyPre - (Arithmetic - { addr_caller - ; addr_callee= addr_pre - ; arith_caller= arith_caller_opt - ; arith_callee= Some arith_callee })) - | Satisfiable (abduce_caller, _abduce_callee) -> - let new_astate = - Option.fold abduce_caller ~init:astate ~f:(fun astate abduce_caller -> - let attribute = - Attribute.Arithmetic - ( abduce_caller - , add_call_to_trace callee_proc_name call_location hist_caller - arith_callee_hist ) - in - Memory.abduce_attribute addr_caller attribute astate - |> Memory.add_attribute addr_caller attribute ) - in - {call_state with astate= new_astate} ) - - (** Materialize the (abstract memory) subgraph of [pre] reachable from [addr_pre] in [call_state.astate] starting from address [addr_caller]. Report an error if some invalid addresses are traversed in the process. *) @@ -495,11 +458,7 @@ module PrePost = struct match BaseMemory.find_opt addr_pre pre.BaseDomain.heap with | None -> Ok call_state - | Some (edges_pre, attrs_pre) -> - let call_state = - solve_arithmetic_constraints callee_proc_name call_location ~addr_pre ~attrs_pre - ~addr_hist_caller call_state - in + | Some (edges_pre, _attrs_pre) -> Container.fold_result ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold) ~init:call_state edges_pre ~f:(fun call_state (access, (addr_pre_dest, _)) -> @@ -574,15 +533,92 @@ module PrePost = struct ~addr_pre ~addr_hist_caller call_state ) + let translate_attributes attrs_callee subst = + let translate_attribute subst attr = + match (attr : Attribute.t) with + | BoItv itv -> + let subst, itv' = Itv.subst_pulse_values subst itv in + (subst, Attribute.BoItv itv') + | AddressOfCppTemporary _ + | AddressOfStackVariable _ + | Arithmetic _ + | Closure _ + | Invalid _ + | MustBeValid _ + | StdVectorReserve + | WrittenTo _ -> + (* non-relational attributes *) + (subst, attr) + in + Attributes.fold_map attrs_callee ~init:subst ~f:translate_attribute + + + let solve_arithmetic_constraints callee_proc_name call_location ~addr_pre ~attrs_pre + ~addr_hist_caller call_state = + match Attributes.get_arithmetic attrs_pre with + | None -> + call_state + | Some (arith_callee, arith_callee_hist) -> ( + let addr_caller, hist_caller = addr_hist_caller in + let astate = call_state.astate in + let arith_caller_opt = Memory.get_arithmetic addr_caller astate |> Option.map ~f:fst in + (* TODO: we don't use [abduced_callee] but we could probably use it to refine the attributes + for that address in the post since abstract values are immutable *) + match + Arithmetic.abduce_binop_is_true ~negated:false Eq arith_caller_opt (Some arith_callee) + with + | Unsatisfiable -> + raise + (CannotApplyPre + (Arithmetic + { addr_caller + ; addr_callee= addr_pre + ; arith_caller= arith_caller_opt + ; arith_callee= Some arith_callee })) + | Satisfiable (abduce_caller, _abduce_callee) -> + let new_astate = + Option.fold abduce_caller ~init:astate ~f:(fun astate abduce_caller -> + let attribute = + Attribute.Arithmetic + ( abduce_caller + , add_call_to_trace callee_proc_name call_location hist_caller + arith_callee_hist ) + in + Memory.abduce_attribute addr_caller attribute astate + |> Memory.add_attribute addr_caller attribute ) + in + {call_state with astate= new_astate} ) + + + 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 + solve_arithmetic_constraints callee_proc_name call_location ~addr_pre ~attrs_pre + ~addr_hist_caller {call_state with subst} + in + (* check all callee addresses that make sense for the caller, i.e. the domain of [call_state.subst] *) + AddressMap.fold + (fun addr_callee addr_hist_caller call_state -> + match BaseMemory.find_opt addr_callee (pre_post.pre :> BaseDomain.t).heap with + | None -> + call_state + | Some (_edges, callee_attrs) -> + one_address_sat addr_callee callee_attrs addr_hist_caller call_state ) + call_state.subst call_state + + let materialize_pre callee_proc_name call_location pre_post ~formals ~actuals call_state = + let ( >>= ) x f = Option.map x ~f:(Result.bind ~f) in + let ( >>| ) x f = Option.map x ~f:(Result.map ~f) in PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call pre" ())) ; let r = + (* first make as large a mapping as we can between callee values and caller values... *) materialize_pre_for_parameters callee_proc_name call_location pre_post ~formals ~actuals call_state - |> Option.map - ~f: - (Result.bind ~f:(fun call_state -> - materialize_pre_for_globals callee_proc_name call_location pre_post call_state )) + >>= materialize_pre_for_globals callee_proc_name call_location pre_post + >>| (* ...then relational arithmetic constraints in the callee's attributes will make sense in + terms of the caller's values *) + apply_arithmetic_constraints callee_proc_name call_location pre_post in PerfEvent.(log (fun logger -> log_end_event logger ())) ; r @@ -627,21 +663,26 @@ module PrePost = struct old_post_edges edges_pre ) - let add_call_to_attr proc_name call_location caller_history attr = - match (attr : Attribute.t) with - | Invalid (invalidation, trace) -> - Attribute.Invalid - (invalidation, add_call_to_trace proc_name call_location caller_history trace) - | Arithmetic (arith, trace) -> - Attribute.Arithmetic (arith, add_call_to_trace proc_name call_location caller_history trace) - | AddressOfCppTemporary (_, _) - | AddressOfStackVariable (_, _, _) - | BoItv _ - | Closure _ - | MustBeValid _ - | StdVectorReserve - | WrittenTo _ -> - attr + let add_call_to_attributes proc_name call_location caller_history attrs call_state = + let add_call_to_attribute attr = + match (attr : Attribute.t) with + | Invalid (invalidation, trace) -> + Attribute.Invalid + (invalidation, add_call_to_trace proc_name call_location caller_history trace) + | Arithmetic (arith, trace) -> + Attribute.Arithmetic + (arith, add_call_to_trace proc_name call_location caller_history trace) + | AddressOfCppTemporary (_, _) + | AddressOfStackVariable (_, _, _) + | BoItv _ + | Closure _ + | MustBeValid _ + | StdVectorReserve + | WrittenTo _ -> + attr + in + let call_state, attrs = translate_attributes attrs call_state in + (call_state, Attributes.map attrs ~f:(fun attr -> add_call_to_attribute attr)) let record_post_cell callee_proc_name call_loc ~addr_callee ~cell_pre_opt @@ -650,16 +691,14 @@ module PrePost = struct delete_edges_in_callee_pre_from_caller ~addr_callee ~cell_pre_opt ~addr_caller call_state in let heap = (call_state.astate.post :> base_domain).heap in - let heap = - let attrs_post_caller = - Attributes.map attrs_post ~f:(fun attr -> - add_call_to_attr callee_proc_name call_loc hist_caller attr ) + let subst, heap = + let subst, attrs_post_caller = + add_call_to_attributes callee_proc_name call_loc hist_caller attrs_post call_state.subst in - BaseMemory.set_attrs addr_caller attrs_post_caller heap + (subst, BaseMemory.set_attrs addr_caller attrs_post_caller heap) in let subst, translated_post_edges = - BaseMemory.Edges.fold_map ~init:call_state.subst edges_post - ~f:(fun subst (addr_callee, trace_post) -> + BaseMemory.Edges.fold_map ~init:subst edges_post ~f:(fun subst (addr_callee, trace_post) -> let subst, (addr_curr, hist_curr) = subst_find_or_new subst addr_callee ~default_hist_caller:hist_caller in @@ -812,28 +851,25 @@ module PrePost = struct let record_post_remaining_attributes callee_proc_name call_loc pre_post call_state = let heap0 = (call_state.astate.post :> base_domain).heap in - let heap = + let subst, heap = BaseMemory.fold_attrs - (fun addr_callee attrs heap -> + (fun addr_callee attrs (subst, heap) -> if AddressSet.mem addr_callee call_state.visited then - (* already recorded the attributes when we were walking the edges map *) heap + (* already recorded the attributes when we were walking the edges map *) + (subst, heap) else match AddressMap.find_opt addr_callee call_state.subst with | None -> - (* callee address has no meaning for the caller *) heap + (* callee address has no meaning for the caller *) (subst, heap) | Some (addr_caller, history) -> - let attrs' = - Attributes.map - ~f:(fun attr -> add_call_to_attr callee_proc_name call_loc history attr) - attrs + let subst, attrs' = + add_call_to_attributes callee_proc_name call_loc history attrs subst in - BaseMemory.set_attrs addr_caller attrs' heap ) - (pre_post.post :> BaseDomain.t).heap heap0 + (subst, BaseMemory.set_attrs addr_caller attrs' heap) ) + (pre_post.post :> BaseDomain.t).heap (call_state.subst, heap0) in - if phys_equal heap heap0 then call_state - else - let post = Domain.make (call_state.astate.post :> BaseDomain.t).stack heap in - {call_state with astate= {call_state.astate with post}} + let post = Domain.make (call_state.astate.post :> BaseDomain.t).stack heap in + {call_state with subst; astate= {call_state.astate with post}} let apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state =