From 5b0fd3af6fa5df23a853d5828fe40556c83d57fd Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Fri, 14 Feb 2020 03:18:12 -0800 Subject: [PATCH] [inferbo] Distinguish unreachable and error status Summary: In Inferbo, the bottom memory is introduced when a node is unreachable by pruning, i.e. `[[e]] <= [0,0]` on `prune(e)`. This diff distinguishes whether `[[e]]` is `[0,0]` (unreachable) or bottom (it could not evaluate `e` by some unknown reasons). Reviewed By: ezgicicek Differential Revision: D19902046 fbshipit-source-id: 7706017d6 --- .../bufferoverrun/bufferOverrunAnalysis.ml | 4 +- .../src/bufferoverrun/bufferOverrunChecker.ml | 8 +- .../src/bufferoverrun/bufferOverrunDomain.ml | 73 +++++++++++-------- .../src/bufferoverrun/bufferOverrunDomain.mli | 11 ++- .../src/bufferoverrun/bufferOverrunModels.ml | 2 +- .../bufferoverrun/bufferOverrunSemantics.ml | 24 +++--- infer/src/cost/boundMap.ml | 10 ++- 7 files changed, 80 insertions(+), 52 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index ecae2f581..892da89d6 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -72,7 +72,7 @@ module TransferFunctions = struct if Dom.LatestPrune.is_top latest_prune' then mem else Dom.Mem.set_latest_prune latest_prune' mem | Error `SubstBottom -> - Dom.Mem.bot + Dom.Mem.unreachable | Error `SubstFail -> mem @@ -476,7 +476,7 @@ let compute_summary : (Pvar.t * Typ.t) list -> CFG.t -> invariant_map -> memory_ | Some exit_mem -> exit_mem |> Dom.Mem.forget_unreachable_locs ~formals |> Dom.Mem.unset_oenv | None -> - Bottom + Unreachable let do_analysis : Callbacks.proc_callback_args -> Summary.t = diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 55dee0dc6..db697681d 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -342,16 +342,16 @@ let check_instrs : match state with | _ when Instrs.is_empty instrs -> checks - | {AbstractInterpreter.State.pre= Dom.Mem.(Bottom | ExcRaised)} -> + | {AbstractInterpreter.State.pre= Dom.Mem.(Unreachable | Error | ExcRaised)} -> checks - | {AbstractInterpreter.State.pre= Dom.Mem.NonBottom _ as pre; post} -> + | {AbstractInterpreter.State.pre= Reachable _ as pre; post} -> if Instrs.nth_exists instrs 1 then L.(die InternalError) "Did not expect several instructions" ; let instr = Instrs.nth_exn instrs 0 in let checks = match post with - | Dom.Mem.(Bottom | ExcRaised) -> + | Dom.Mem.(Unreachable | ExcRaised) -> add_unreachable_code cfg node instr Instrs.empty checks - | Dom.Mem.NonBottom _ -> + | Dom.Mem.(Error | Reachable _) -> checks in let cond_set = diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 93627a9fc..5930e2efb 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -2333,13 +2333,15 @@ module MemReach = struct end module Mem = struct - type 'has_oenv t0 = Bottom | ExcRaised | NonBottom of 'has_oenv MemReach.t0 + type 'has_oenv t0 = Unreachable | Error | ExcRaised | Reachable of 'has_oenv MemReach.t0 type no_oenv_t = GOption.none t0 type t = GOption.some t0 - let bot : t = Bottom + let unreachable : t = Unreachable + + let error : t = Error let exc_raised : t = ExcRaised @@ -2349,15 +2351,19 @@ module Mem = struct if phys_equal lhs rhs then true else match (lhs, rhs) with - | Bottom, _ -> + | Unreachable, _ -> + true + | _, Unreachable -> + false + | Error, _ -> true - | _, Bottom -> + | _, Error -> false | ExcRaised, _ -> true | _, ExcRaised -> false - | NonBottom lhs, NonBottom rhs -> + | Reachable lhs, Reachable rhs -> MemReach.leq ~lhs ~rhs @@ -2365,33 +2371,37 @@ module Mem = struct if phys_equal x y then x else match (x, y) with - | Bottom, m | m, Bottom -> + | Unreachable, m | m, Unreachable -> + m + | Error, m | m, Error -> m | ExcRaised, m | m, ExcRaised -> m - | NonBottom m1, NonBottom m2 -> - PhysEqual.optim2 ~res:(NonBottom (MemReach.join m1 m2)) x y + | Reachable m1, Reachable m2 -> + PhysEqual.optim2 ~res:(Reachable (MemReach.join m1 m2)) x y let widen ~prev:prev0 ~next:next0 ~num_iters = if phys_equal prev0 next0 then prev0 else match (prev0, next0) with - | Bottom, m | m, Bottom -> + | Unreachable, m | m, Unreachable -> + m + | Error, m | m, Error -> m | ExcRaised, m | m, ExcRaised -> m - | NonBottom prev, NonBottom next -> - PhysEqual.optim2 ~res:(NonBottom (MemReach.widen ~prev ~next ~num_iters)) prev0 next0 + | Reachable prev, Reachable next -> + PhysEqual.optim2 ~res:(Reachable (MemReach.widen ~prev ~next ~num_iters)) prev0 next0 let map ~f x = match x with - | Bottom | ExcRaised -> + | Unreachable | Error | ExcRaised -> x - | NonBottom m -> + | Reachable m -> let m' = f m in - if phys_equal m' m then x else NonBottom m' + if phys_equal m' m then x else Reachable m' type get_summary = Procname.t -> no_oenv_t option @@ -2399,13 +2409,14 @@ module Mem = struct let init : get_summary -> OndemandEnv.t -> t = fun get_summary oenv -> let get_summary pname = - match get_summary pname with Some (NonBottom m) -> Some m | _ -> None + match get_summary pname with Some (Reachable m) -> Some m | _ -> None in - NonBottom (MemReach.init get_summary oenv) + Reachable (MemReach.init get_summary oenv) let f_lift_default : default:'a -> ('h MemReach.t0 -> 'a) -> 'h t0 -> 'a = - fun ~default f m -> match m with Bottom | ExcRaised -> default | NonBottom m' -> f m' + fun ~default f m -> + match m with Unreachable | Error | ExcRaised -> default | Reachable m' -> f m' let is_stack_loc : Loc.t -> _ t0 -> bool = @@ -2450,9 +2461,9 @@ module Mem = struct let find_ret_alias : _ t0 -> AliasTargets.t bottom_lifted = fun m -> match m with - | Bottom | ExcRaised -> + | Unreachable | Error | ExcRaised -> Bottom - | NonBottom m' -> + | Reachable m' -> NonBottom (MemReach.find_ret_alias m') @@ -2503,8 +2514,8 @@ module Mem = struct let incr_iterator_simple_alias_on_call eval_sym_trace ~callee_exit_mem m = match (callee_exit_mem, m) with - | NonBottom callee_exit_mem, NonBottom m -> - NonBottom (MemReach.incr_iterator_simple_alias_on_call eval_sym_trace ~callee_exit_mem m) + | Reachable callee_exit_mem, Reachable m -> + Reachable (MemReach.incr_iterator_simple_alias_on_call eval_sym_trace ~callee_exit_mem m) | _, _ -> m @@ -2556,11 +2567,11 @@ module Mem = struct let apply_latest_prune : Exp.t -> t -> t * PrunePairs.t = fun e -> function - | (Bottom | ExcRaised) as x -> + | (Unreachable | Error | ExcRaised) as x -> (x, PrunePairs.empty) - | NonBottom m -> + | Reachable m -> let m, prune_pairs = MemReach.apply_latest_prune e m in - (NonBottom m, prune_pairs) + (Reachable m, prune_pairs) let update_latest_prune : updated_locs:PowLoc.t -> Exp.t -> Exp.t -> t -> t = @@ -2582,10 +2593,10 @@ module Mem = struct let forget_size_alias arr_locs = map ~f:(MemReach.forget_size_alias arr_locs) let unset_oenv = function - | (Bottom | ExcRaised) as x -> + | (Unreachable | Error | ExcRaised) as x -> x - | NonBottom m -> - NonBottom (MemReach.unset_oenv m) + | Reachable m -> + Reachable (MemReach.unset_oenv m) let set_first_idx_of_null loc idx = map ~f:(MemReach.set_first_idx_of_null loc idx) @@ -2601,10 +2612,12 @@ module Mem = struct let pp f m = match m with - | Bottom -> - F.pp_print_string f SpecialChars.up_tack + | Unreachable -> + F.fprintf f "%s_unreachable" SpecialChars.up_tack + | Error -> + F.fprintf f "%s_our_fault" SpecialChars.up_tack | ExcRaised -> F.pp_print_string f (SpecialChars.up_tack ^ " by exception") - | NonBottom m -> + | Reachable m -> MemReach.pp f m end diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.mli b/infer/src/bufferoverrun/bufferOverrunDomain.mli index df5c3e9b9..c225eda5a 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.mli +++ b/infer/src/bufferoverrun/bufferOverrunDomain.mli @@ -460,10 +460,13 @@ end module Mem : sig type 'has_oenv t0 = - | Bottom (** Memory of unreachable node *) + | Unreachable (** Memory of unreachable node *) + | Error + (** Error status due to Inferbo's incorrect semantics/models, e.g., when a value of an + abstract location is not found from the abstract memory inadvertently *) | ExcRaised (** Memory of node that can be reachable only with exception raises that we want to ignore *) - | NonBottom of 'has_oenv MemReach.t0 + | Reachable of 'has_oenv MemReach.t0 (** Memory type without an environment for on-demand symbol evaluation *) type no_oenv_t = GOption.none t0 @@ -477,7 +480,9 @@ module Mem : sig val pp : Format.formatter -> _ t0 -> unit - val bot : t + val unreachable : t + + val error : t type get_summary = Procname.t -> no_oenv_t option diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index aed729535..24cc8412b 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -373,7 +373,7 @@ let by_risky_value_from lib_fun = let bottom = - let exec _model_env ~ret:_ _mem = Dom.Mem.bot in + let exec _model_env ~ret:_ _mem = Dom.Mem.unreachable in {exec; check= no_check} diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index ca33eab7e..6d0274e19 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -748,17 +748,20 @@ module Prune = struct astate - let is_unreachable_constant : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> bool = - fun integer_type_widths e m -> - let v = eval integer_type_widths e m in - Itv.leq ~lhs:(Val.get_itv v) ~rhs:(Itv.of_int 0) - && PowLoc.is_bot (Val.get_pow_loc v) - && ArrayBlk.is_bot (Val.get_array_blk v) - - let prune_unreachable : Typ.IntegerWidths.t -> Exp.t -> t -> t = fun integer_type_widths e ({mem} as astate) -> - if is_unreachable_constant integer_type_widths e mem then {astate with mem= Mem.bot} else astate + match mem with + | Mem.(Unreachable | Error | ExcRaised) -> + astate + | Mem.Reachable _ -> + let v = eval integer_type_widths e mem in + let itv_v = Val.get_itv v in + if + Itv.leq ~lhs:itv_v ~rhs:(Itv.of_int 0) + && PowLoc.is_bot (Val.get_pow_loc v) + && ArrayBlk.is_bot (Val.get_array_blk v) + then {astate with mem= (if Itv.is_bottom itv_v then Mem.error else Mem.unreachable)} + else astate let rec prune_helper integer_type_widths e astate = @@ -804,5 +807,6 @@ module Prune = struct fun integer_type_widths e mem -> let mem, prune_pairs = Mem.apply_latest_prune e mem in let {mem; prune_pairs} = prune_helper integer_type_widths e {mem; prune_pairs} in - if PrunePairs.is_reachable prune_pairs then Mem.set_prune_pairs prune_pairs mem else Mem.bot + if PrunePairs.is_reachable prune_pairs then Mem.set_prune_pairs prune_pairs mem + else Mem.unreachable end diff --git a/infer/src/cost/boundMap.ml b/infer/src/cost/boundMap.ml index ae5713bad..10f0dd49f 100644 --- a/infer/src/cost/boundMap.ml +++ b/infer/src/cost/boundMap.ml @@ -55,15 +55,21 @@ let compute_upperbound_map node_cfg inferbo_invariant_map control_invariant_map (* bound = env(v1) *... * env(vn) *) let bound = match entry_mem with - | Bottom -> + | Unreachable -> L.debug Analysis Medium "@\n\ [COST ANALYSIS INTERNAL WARNING:] No 'env' found. This location is \ unreachable returning cost 0 \n" ; BasicCost.zero + | Error -> + L.debug Analysis Medium + "@\n\ + [COST ANALYSIS INTERNAL WARNING:] No 'env' found. The Inferbo memory of this \ + location is erroneous \n" ; + BasicCost.zero | ExcRaised -> BasicCost.one - | NonBottom mem -> + | Reachable mem -> let cost = BufferOverrunDomain.MemReach.range ~filter_loc:(filter_loc control_map) ~node_id mem