From a152a6131b8ea065c3215ba819f61d702faac4dd Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 9 Apr 2020 01:18:46 -0700 Subject: [PATCH] [inferbo] Give a right location to traces for pruning Summary: The pruning location of array size was dummy. This diff gives a right location to traces in the pruning. Reviewed By: ezgicicek Differential Revision: D20915167 fbshipit-source-id: 55cc583df --- .../bufferoverrun/bufferOverrunAnalysis.ml | 4 +- .../src/bufferoverrun/bufferOverrunModels.ml | 4 +- .../bufferoverrun/bufferOverrunSemantics.ml | 69 ++++++++++--------- .../bufferoverrun/bufferOverrunSemantics.mli | 7 +- 4 files changed, 46 insertions(+), 38 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index 890072216..ba9dad24d 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -373,8 +373,8 @@ module TransferFunctions = struct in let mem = Dom.Mem.update_latest_prune ~updated_locs:locs exp1 exp2 mem in mem - | Prune (exp, _, _, _) -> - Sem.Prune.prune integer_type_widths exp mem + | Prune (exp, location, _, _) -> + Sem.Prune.prune location integer_type_widths exp mem | Call ((id, _), Const (Cfun callee_pname), _, _, _) when is_java_enum_values tenv callee_pname -> let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 673cd32bc..5fe21fc5c 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -1201,7 +1201,9 @@ end module Preconditions = struct let check_argument exp = - let exec {integer_type_widths} ~ret:_ mem = Sem.Prune.prune integer_type_widths exp mem in + let exec {integer_type_widths; location} ~ret:_ mem = + Sem.Prune.prune location integer_type_widths exp mem + in {exec; check= no_check} end diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 24f114f4f..1d665a288 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -624,7 +624,7 @@ module Prune = struct astate - let gen_prune_alias_functions ~prune_alias_core integer_type_widths comp x e astate = + let gen_prune_alias_functions ~prune_alias_core location integer_type_widths comp x e astate = (* [val_prune_eq] is applied when the alias type is [AliasTarget.Eq]. *) let val_prune_eq = match (comp : Binop.t) with @@ -655,12 +655,13 @@ module Prune = struct assert false in let make_pruning_exp = PruningExp.make comp in - prune_alias_core ~val_prune_eq ~val_prune_le ~make_pruning_exp integer_type_widths x e astate + prune_alias_core ~val_prune_eq ~val_prune_le ~make_pruning_exp location integer_type_widths x e + astate let prune_simple_alias = - let prune_alias_core ~val_prune_eq ~val_prune_le:_ ~make_pruning_exp integer_type_widths x e - ({mem} as astate) = + let prune_alias_core ~val_prune_eq ~val_prune_le:_ ~make_pruning_exp _location + integer_type_widths x e ({mem} as astate) = List.fold (Mem.find_simple_alias x mem) ~init:astate ~f:(fun acc (lv, i) -> let lhs = Mem.find lv mem in let rhs = @@ -677,8 +678,8 @@ module Prune = struct let prune_size_alias = - let prune_alias_core ~val_prune_eq ~val_prune_le ~make_pruning_exp integer_type_widths x e - ({mem} as astate) = + let prune_alias_core ~val_prune_eq ~val_prune_le ~make_pruning_exp location integer_type_widths + x e ({mem} as astate) = List.fold (Mem.find_size_alias x mem) ~init:astate ~f:(fun astate (alias_typ, lv, i, java_tmp) -> let array_v = Mem.find lv mem in @@ -693,9 +694,7 @@ module Prune = struct let prune_target val_prune astate = let lhs' = val_prune lhs rhs in let array_v' = - Val.set_array_length Location.dummy - ~length:(Val.minus_a lhs' (Val.of_int_lit i)) - array_v + Val.set_array_length location ~length:(Val.minus_a lhs' (Val.of_int_lit i)) array_v in let pruning_exp = make_pruning_exp ~lhs:lhs' ~rhs in (update_mem_in_prune lv array_v' ~pruning_exp astate, lhs', pruning_exp) @@ -718,17 +717,17 @@ module Prune = struct gen_prune_alias_functions ~prune_alias_core - let rec prune_binop_left : Typ.IntegerWidths.t -> Exp.t -> t -> t = - fun integer_type_widths e astate -> + let rec prune_binop_left : Location.t -> Typ.IntegerWidths.t -> Exp.t -> t -> t = + fun location integer_type_widths e astate -> match e with | Exp.BinOp (comp, Exp.Cast (_, e1), e2) -> - prune_binop_left integer_type_widths (Exp.BinOp (comp, e1, e2)) astate + prune_binop_left location integer_type_widths (Exp.BinOp (comp, e1, e2)) astate | Exp.BinOp (((Binop.Lt | Binop.Gt | Binop.Le | Binop.Ge | Binop.Eq | Binop.Ne) as comp), Exp.Var x, e') -> astate - |> prune_simple_alias integer_type_widths comp x e' - |> prune_size_alias integer_type_widths comp x e' + |> prune_simple_alias location integer_type_widths comp x e' + |> prune_size_alias location integer_type_widths comp x e' | Exp.BinOp ( ((Binop.Lt | Binop.Gt | Binop.Le | Binop.Ge | Binop.Eq | Binop.Ne) as comp) , Exp.BinOp (Binop.PlusA t, e1, e2) @@ -737,29 +736,29 @@ module Prune = struct Be careful when you take into account integer overflows in the abstract semantics [eval] in the future. *) astate - |> prune_binop_left integer_type_widths + |> prune_binop_left location integer_type_widths (Exp.BinOp (comp, e1, Exp.BinOp (Binop.MinusA t, e3, e2))) - |> prune_binop_left integer_type_widths + |> prune_binop_left location integer_type_widths (Exp.BinOp (comp, e2, Exp.BinOp (Binop.MinusA t, e3, e1))) | Exp.BinOp ( ((Binop.Lt | Binop.Gt | Binop.Le | Binop.Ge | Binop.Eq | Binop.Ne) as comp) , Exp.BinOp (Binop.MinusA t, e1, e2) , e3 ) -> astate - |> prune_binop_left integer_type_widths + |> prune_binop_left location integer_type_widths (Exp.BinOp (comp, e1, Exp.BinOp (Binop.PlusA t, e3, e2))) - |> prune_binop_left integer_type_widths + |> prune_binop_left location integer_type_widths (Exp.BinOp (comp_rev comp, e2, Exp.BinOp (Binop.MinusA t, e1, e3))) | _ -> astate - let prune_binop_right : Typ.IntegerWidths.t -> Exp.t -> t -> t = - fun integer_type_widths e astate -> + let prune_binop_right : Location.t -> Typ.IntegerWidths.t -> Exp.t -> t -> t = + fun location integer_type_widths e astate -> match e with | Exp.BinOp (((Binop.Lt | Binop.Gt | Binop.Le | Binop.Ge | Binop.Eq | Binop.Ne) as c), e1, e2) -> - prune_binop_left integer_type_widths (Exp.BinOp (comp_rev c, e2, e1)) astate + prune_binop_left location integer_type_widths (Exp.BinOp (comp_rev c, e2, e1)) astate | _ -> astate @@ -786,13 +785,13 @@ module Prune = struct else astate - let rec prune_helper integer_type_widths e astate = + let rec prune_helper location integer_type_widths e astate = let astate = astate |> prune_unreachable integer_type_widths e |> prune_unop e - |> prune_binop_left integer_type_widths e - |> prune_binop_right integer_type_widths e + |> prune_binop_left location integer_type_widths e + |> prune_binop_right location integer_type_widths e in let is_const_zero x = match Exp.ignore_integer_cast x with @@ -803,32 +802,34 @@ module Prune = struct in match e with | Exp.BinOp (Binop.Ne, e1, e2) when is_const_zero e2 -> - prune_helper integer_type_widths e1 astate + prune_helper location integer_type_widths e1 astate | Exp.BinOp (Binop.Eq, e1, e2) when is_const_zero e2 -> - prune_helper integer_type_widths (Exp.UnOp (Unop.LNot, e1, None)) astate + prune_helper location integer_type_widths (Exp.UnOp (Unop.LNot, e1, None)) astate | Exp.UnOp (Unop.Neg, Exp.Var x, _) -> - prune_helper integer_type_widths (Exp.Var x) astate + prune_helper location integer_type_widths (Exp.Var x) astate | Exp.BinOp (Binop.LAnd, e1, e2) -> - astate |> prune_helper integer_type_widths e1 |> prune_helper integer_type_widths e2 + astate + |> prune_helper location integer_type_widths e1 + |> prune_helper location integer_type_widths e2 | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.LOr, e1, e2), t) -> astate - |> prune_helper integer_type_widths (Exp.UnOp (Unop.LNot, e1, t)) - |> prune_helper integer_type_widths (Exp.UnOp (Unop.LNot, e2, t)) + |> prune_helper location integer_type_widths (Exp.UnOp (Unop.LNot, e1, t)) + |> prune_helper location integer_type_widths (Exp.UnOp (Unop.LNot, e2, t)) | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Lt as c), e1, e2), _) | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Gt as c), e1, e2), _) | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Le as c), e1, e2), _) | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Ge as c), e1, e2), _) | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Eq as c), e1, e2), _) | Exp.UnOp (Unop.LNot, Exp.BinOp ((Binop.Ne as c), e1, e2), _) -> - prune_helper integer_type_widths (Exp.BinOp (comp_not c, e1, e2)) astate + prune_helper location integer_type_widths (Exp.BinOp (comp_not c, e1, e2)) astate | _ -> astate - let prune : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Mem.t = - fun integer_type_widths e mem -> + let prune : Location.t -> Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Mem.t = + fun location 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 + let {mem; prune_pairs} = prune_helper location integer_type_widths e {mem; prune_pairs} in if PrunePairs.is_reachable prune_pairs then Mem.set_prune_pairs prune_pairs mem else Mem.unreachable end diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.mli b/infer/src/bufferoverrun/bufferOverrunSemantics.mli index 945759e95..0e6239153 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.mli +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.mli @@ -80,6 +80,11 @@ val mk_eval_sym_cost : (** Make [eval_sym] function of [EvalCost] mode for on-demand symbol evaluation *) module Prune : sig - val prune : Typ.IntegerWidths.t -> Exp.t -> BufferOverrunDomain.Mem.t -> BufferOverrunDomain.Mem.t + val prune : + Location.t + -> Typ.IntegerWidths.t + -> Exp.t + -> BufferOverrunDomain.Mem.t + -> BufferOverrunDomain.Mem.t (** Prune memory with the given condition expression *) end