From da7cd0b45aeb7db6de1724fd22cae4d9a627df06 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 24 Feb 2020 08:45:14 -0800 Subject: [PATCH] [inferbo] Ignore error memory status Summary: This ignores the error memory status (e.g. when condition expression is evaluated to bottom), in order to keep analyze following code. ``` if ( e ) // e is evaluated to bottom due to a problem of Inferbo { ... // code here was not analyzed before } ``` Reviewed By: ezgicicek Differential Revision: D20067434 fbshipit-source-id: a1713722c --- .../src/bufferoverrun/bufferOverrunChecker.ml | 4 +-- .../src/bufferoverrun/bufferOverrunDomain.ml | 25 +++++-------------- .../src/bufferoverrun/bufferOverrunDomain.mli | 5 ---- .../bufferoverrun/bufferOverrunSemantics.ml | 10 ++++++-- infer/src/cost/boundMap.ml | 6 ----- 5 files changed, 16 insertions(+), 34 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 67875e465..fcab164fd 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -341,7 +341,7 @@ let check_instrs : match state with | _ when Instrs.is_empty instrs -> checks - | {AbstractInterpreter.State.pre= Dom.Mem.(Unreachable | Error | ExcRaised)} -> + | {AbstractInterpreter.State.pre= Dom.Mem.(Unreachable | ExcRaised)} -> checks | {AbstractInterpreter.State.pre= Reachable _ as pre; post} -> if Instrs.nth_exists instrs 1 then L.(die InternalError) "Did not expect several instructions" ; @@ -350,7 +350,7 @@ let check_instrs : match post with | Dom.Mem.(Unreachable | ExcRaised) -> add_unreachable_code cfg node instr Instrs.empty checks - | Dom.Mem.(Error | Reachable _) -> + | Dom.Mem.Reachable _ -> checks in let cond_set = diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 5f3d4e3bd..58e895b09 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -2332,7 +2332,7 @@ module MemReach = struct end module Mem = struct - type 'has_oenv t0 = Unreachable | Error | ExcRaised | Reachable of 'has_oenv MemReach.t0 + type 'has_oenv t0 = Unreachable | ExcRaised | Reachable of 'has_oenv MemReach.t0 type no_oenv_t = GOption.none t0 @@ -2340,8 +2340,6 @@ module Mem = struct let unreachable : t = Unreachable - let error : t = Error - let exc_raised : t = ExcRaised let is_exc_raised = function ExcRaised -> true | _ -> false @@ -2354,10 +2352,6 @@ module Mem = struct true | _, Unreachable -> false - | Error, _ -> - true - | _, Error -> - false | ExcRaised, _ -> true | _, ExcRaised -> @@ -2372,8 +2366,6 @@ module Mem = struct match (x, y) with | Unreachable, m | m, Unreachable -> m - | Error, m | m, Error -> - m | ExcRaised, m | m, ExcRaised -> m | Reachable m1, Reachable m2 -> @@ -2386,8 +2378,6 @@ module Mem = struct match (prev0, next0) with | Unreachable, m | m, Unreachable -> m - | Error, m | m, Error -> - m | ExcRaised, m | m, ExcRaised -> m | Reachable prev, Reachable next -> @@ -2396,7 +2386,7 @@ module Mem = struct let map ~f x = match x with - | Unreachable | Error | ExcRaised -> + | Unreachable | ExcRaised -> x | Reachable m -> let m' = f m in @@ -2414,8 +2404,7 @@ module Mem = struct let f_lift_default : default:'a -> ('h MemReach.t0 -> 'a) -> 'h t0 -> 'a = - fun ~default f m -> - match m with Unreachable | Error | ExcRaised -> default | Reachable m' -> f m' + fun ~default f m -> match m with Unreachable | ExcRaised -> default | Reachable m' -> f m' let is_stack_loc : Loc.t -> _ t0 -> bool = @@ -2460,7 +2449,7 @@ module Mem = struct let find_ret_alias : _ t0 -> AliasTargets.t bottom_lifted = fun m -> match m with - | Unreachable | Error | ExcRaised -> + | Unreachable | ExcRaised -> Bottom | Reachable m' -> NonBottom (MemReach.find_ret_alias m') @@ -2566,7 +2555,7 @@ module Mem = struct let apply_latest_prune : Exp.t -> t -> t * PrunePairs.t = fun e -> function - | (Unreachable | Error | ExcRaised) as x -> + | (Unreachable | ExcRaised) as x -> (x, PrunePairs.empty) | Reachable m -> let m, prune_pairs = MemReach.apply_latest_prune e m in @@ -2592,7 +2581,7 @@ module Mem = struct let forget_size_alias arr_locs = map ~f:(MemReach.forget_size_alias arr_locs) let unset_oenv = function - | (Unreachable | Error | ExcRaised) as x -> + | (Unreachable | ExcRaised) as x -> x | Reachable m -> Reachable (MemReach.unset_oenv m) @@ -2613,8 +2602,6 @@ module Mem = struct match m with | 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") | Reachable m -> diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.mli b/infer/src/bufferoverrun/bufferOverrunDomain.mli index 3f07c2a90..c14875574 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.mli +++ b/infer/src/bufferoverrun/bufferOverrunDomain.mli @@ -464,9 +464,6 @@ end module Mem : sig type 'has_oenv t0 = | 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 *) | Reachable of 'has_oenv MemReach.t0 @@ -485,8 +482,6 @@ module Mem : sig val unreachable : t - val error : t - type get_summary = Procname.t -> no_oenv_t option val init : get_summary -> BufferOverrunOndemandEnv.t -> t diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index b1d27c8cf..4027562c5 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -753,7 +753,7 @@ module Prune = struct let prune_unreachable : Typ.IntegerWidths.t -> Exp.t -> t -> t = fun integer_type_widths e ({mem} as astate) -> match mem with - | Mem.(Unreachable | Error | ExcRaised) -> + | Mem.(Unreachable | ExcRaised) -> astate | Mem.Reachable _ -> let v = eval integer_type_widths e mem in @@ -762,7 +762,13 @@ module Prune = struct 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)} + then + if Itv.is_bottom itv_v then + let () = + Logging.d_printfln_escaped "Warning: the condition expression is evaluated to bottom" + in + astate + else {astate with mem= Mem.unreachable} else astate diff --git a/infer/src/cost/boundMap.ml b/infer/src/cost/boundMap.ml index 10f0dd49f..4b2b4599c 100644 --- a/infer/src/cost/boundMap.ml +++ b/infer/src/cost/boundMap.ml @@ -61,12 +61,6 @@ let compute_upperbound_map node_cfg inferbo_invariant_map control_invariant_map [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 | Reachable mem ->