From 6759763a983d56bed9a59fa07760fef1d47bdfd9 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 11 Sep 2018 18:28:59 -0700 Subject: [PATCH] [inferbo] Simplify instantiate_ret_alias Summary: It simplifies instantiataion of `ret_alias`. While it got `ret_alias` values by iterating caller's and callee's memory, now it gets `ret_alias` by evaluating symbol paths included in location values. Reviewed By: mbouaziz Differential Revision: D9569606 fbshipit-source-id: a3326bb81 --- infer/src/bufferoverrun/absLoc.ml | 33 +++++++++++-- .../src/bufferoverrun/bufferOverrunChecker.ml | 33 ++++++++----- .../src/bufferoverrun/bufferOverrunDomain.ml | 7 ++- .../src/bufferoverrun/bufferOverrunModels.ml | 13 ++++-- .../bufferoverrun/bufferOverrunSemantics.ml | 46 +++++-------------- infer/src/bufferoverrun/bufferOverrunUtils.ml | 35 ++++++++------ .../src/bufferoverrun/bufferOverrunUtils.mli | 1 + infer/src/bufferoverrun/symb.mli | 1 + 8 files changed, 101 insertions(+), 68 deletions(-) diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 2aca99e2e..1431bbbbe 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -12,7 +12,14 @@ open! IStd module F = Format module Allocsite = struct - type t = Unknown | Known of {proc_name: string; node_hash: int; inst_num: int; dimension: int} + type t = + | Unknown + | Known of + { proc_name: string + ; node_hash: int + ; inst_num: int + ; dimension: int + ; path: Symb.SymbolPath.partial option } [@@deriving compare] let pp fmt = function @@ -24,12 +31,20 @@ module Allocsite = struct let to_string x = F.asprintf "%a" pp x - let make : Typ.Procname.t -> node_hash:int -> inst_num:int -> dimension:int -> t = - fun proc_name ~node_hash ~inst_num ~dimension -> - Known {proc_name= Typ.Procname.to_string proc_name; node_hash; inst_num; dimension} + let make : + Typ.Procname.t + -> node_hash:int + -> inst_num:int + -> dimension:int + -> path:Symb.SymbolPath.partial option + -> t = + fun proc_name ~node_hash ~inst_num ~dimension ~path -> + Known {proc_name= Typ.Procname.to_string proc_name; node_hash; inst_num; dimension; path} let unknown = Unknown + + let get_path = function Unknown -> None | Known {path} -> path end module Loc = struct @@ -84,6 +99,16 @@ module Loc = struct let is_field_of ~loc ~field_loc = match field_loc with Field (l, _) -> equal loc l | _ -> false + + let rec get_path = function + | Var (LogicalVar _) -> + None + | Var (ProgramVar pvar) -> + Some (Symb.SymbolPath.of_pvar pvar) + | Allocsite allocsite -> + Allocsite.get_path allocsite + | Field (l, fn) -> + Option.map (get_path l) ~f:(fun p -> Symb.SymbolPath.field p fn) end module PowLoc = struct diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 879be71b2..a59398c3e 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -34,7 +34,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct type extras = Itv.SymbolTable.t - let instantiate_ret ret callee_pname ~callee_exit_mem eval_sym_trace mem ret_alias location = + let instantiate_ret (id, _) callee_pname ~callee_exit_mem eval_sym_trace + eval_locs_sympath_partial mem location = let copy_reachable_new_locs_from locs mem = let copy loc acc = Option.value_map (Dom.Mem.find_opt loc callee_exit_mem) ~default:acc ~f:(fun v -> @@ -47,15 +48,27 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let reachable_locs = Dom.Mem.get_reachable_locs_from locs callee_exit_mem in PowLoc.fold copy reachable_locs mem in - let id = fst ret in + let instantiate_ret_alias mem = + let subst_loc l = + Option.find_map (Loc.get_path l) ~f:(fun partial -> + try + let locs = eval_locs_sympath_partial partial in + if PowLoc.is_singleton locs then Some (PowLoc.choose locs) else None + with Caml.Not_found -> None ) + in + let ret_alias = + Option.find_map (Dom.Mem.find_ret_alias callee_exit_mem) ~f:(fun alias_target -> + Dom.AliasTarget.loc_map alias_target ~f:subst_loc ) + in + Option.value_map ret_alias ~default:mem ~f:(fun l -> Dom.Mem.load_alias id l mem) + in let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in let ret_val = Dom.Mem.find ret_loc callee_exit_mem in let ret_var = Loc.of_var (Var.of_id id) in - let add_ret_alias l = Dom.Mem.load_alias id l mem in - let mem = Option.value_map ret_alias ~default:mem ~f:add_ret_alias in Dom.Val.subst ret_val eval_sym_trace location |> Dom.Val.add_trace_elem (Trace.Return location) |> Fn.flip (Dom.Mem.add_stack ret_var) mem + |> instantiate_ret_alias |> copy_reachable_new_locs_from (Dom.Val.get_all_locs ret_val) @@ -116,12 +129,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct -> Dom.Mem.astate = fun tenv ret callee_pdesc callee_pname params caller_mem summary location -> let callee_exit_mem = Dom.Summary.get_output summary in - let ret_alias, rel_subst_map = - Sem.get_subst_map tenv callee_pdesc params caller_mem callee_exit_mem - in - let eval_sym_trace = Sem.mk_eval_sym_trace callee_pdesc params caller_mem in + let rel_subst_map = Sem.get_subst_map tenv callee_pdesc params caller_mem callee_exit_mem in + let eval_sym_trace, eval_locpath = Sem.mk_eval_sym_trace callee_pdesc params caller_mem in let caller_mem = - instantiate_ret ret callee_pname ~callee_exit_mem eval_sym_trace caller_mem ret_alias + instantiate_ret ret callee_pname ~callee_exit_mem eval_sym_trace eval_locpath caller_mem location |> instantiate_param tenv callee_pdesc params callee_exit_mem eval_sym_trace location |> forget_ret_relation ret callee_pname @@ -496,10 +507,10 @@ module Report = struct fun tenv callee_pdesc params caller_mem summary location -> let callee_exit_mem = Dom.Summary.get_output summary in let callee_cond = Dom.Summary.get_cond_set summary in - let _, rel_subst_map = Sem.get_subst_map tenv callee_pdesc params caller_mem callee_exit_mem in + let rel_subst_map = Sem.get_subst_map tenv callee_pdesc params caller_mem callee_exit_mem in let pname = Procdesc.get_proc_name callee_pdesc in let caller_rel = Dom.Mem.get_relation caller_mem in - let eval_sym_trace = Sem.mk_eval_sym_trace callee_pdesc params caller_mem in + let eval_sym_trace, _ = Sem.mk_eval_sym_trace callee_pdesc params caller_mem in PO.ConditionSet.subst callee_cond eval_sym_trace rel_subst_map caller_rel pname location diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 2d684c089..a44e74888 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -348,7 +348,12 @@ module AliasTarget = struct let use l = function Simple l' | Empty l' -> Loc.equal l l' - let replace l = function Simple _ -> Simple l | Empty _ -> Empty l + let loc_map x ~f = + match x with + | Simple l -> + Option.map (f l) ~f:(fun l -> Simple l) + | Empty l -> + Option.map (f l) ~f:(fun l -> Empty l) end (* Relations between values of logical variables(registers) and diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 5b449d297..30dea0da2 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -109,7 +109,8 @@ let malloc size_exp = let typ, stride, length0, dyn_length = get_malloc_info size_exp in let length = Sem.eval length0 mem in let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces length) in - let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 in + let path = Option.value_map (Dom.Mem.find_simple_alias id mem) ~default:None ~f:Loc.get_path in + let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path in let offset, size = (Itv.zero, Dom.Val.get_itv length) in let size_exp_opt = let size_exp = Option.value dyn_length ~default:length0 in @@ -120,7 +121,7 @@ let malloc size_exp = |> Dom.Mem.add_stack (Loc.of_id id) v |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt |> set_uninitialized location typ (Dom.Val.get_array_locs v) - |> BoUtils.Exec.init_array_fields tenv pname ~node_hash typ (Dom.Val.get_array_locs v) + |> BoUtils.Exec.init_array_fields tenv pname path ~node_hash typ (Dom.Val.get_array_locs v) ?dyn_length and check = check_alloc_size size_exp in {exec; check} @@ -219,7 +220,8 @@ let set_array_length array length_exp = | Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {elt; stride}} -> let length = Sem.eval length_exp mem |> Dom.Val.get_itv in let stride = Option.map ~f:IntLit.to_int_exn stride in - let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 in + let path = Some (Symb.SymbolPath.of_pvar array_pvar) in + let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path in let v = Dom.Val.of_array_alloc allocsite ~stride ~offset:Itv.zero ~size:length in mem |> Dom.Mem.add_stack (Loc.of_pvar array_pvar) v @@ -349,7 +351,10 @@ module Collection = struct let new_list _ = let exec {pname; node_hash; location} ~ret:(id, _) mem = let loc = Loc.of_id id in - let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 in + let path = + Option.value_map (Dom.Mem.find_simple_alias id mem) ~default:None ~f:Loc.get_path + in + let allocsite = Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path in let alloc_loc = Loc.of_allocsite allocsite in let init_size = Dom.Val.of_int 0 in let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces init_size) in diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 249102d0c..849066295 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -347,11 +347,12 @@ let mk_eval_sym_trace callee_pdesc actual_exps caller_mem = in let eval_sym s = fst (eval_sym_traced s) in let trace_of_sym s = snd (eval_sym_traced s) in - (eval_sym, trace_of_sym) + let eval_locpath partial = eval_locpath params partial caller_mem in + ((eval_sym, trace_of_sym), eval_locpath) let mk_eval_sym callee_pdesc actual_exps caller_mem = - fst (mk_eval_sym_trace callee_pdesc actual_exps caller_mem) + fst (fst (mk_eval_sym_trace callee_pdesc actual_exps caller_mem)) let get_sym_f mem e = Val.get_sym (eval e mem) @@ -510,9 +511,8 @@ let get_matching_pairs : -> Typ.t -> Mem.astate -> Mem.astate - -> AliasTarget.t option * (Relation.Var.t * Relation.SymExp.t option) list = + -> (Relation.Var.t * Relation.SymExp.t option) list = fun tenv callee_v actual actual_exp_opt typ caller_mem callee_exit_mem -> - let callee_ret_alias = Mem.find_ret_alias callee_exit_mem in let get_offset_sym v = Val.get_offset_sym v in let get_size_sym v = Val.get_size_sym v in let get_field_name (fn, _, _) = fn in @@ -523,17 +523,6 @@ let get_matching_pairs : let locs = if PowLoc.is_empty array_locs then Val.get_pow_loc v else array_locs in Mem.find_set locs mem in - let ret_alias = ref None in - let add_ret_alias v1 v2 = - match callee_ret_alias with - | Some ret_loc -> - if - PowLoc.is_singleton v1 && PowLoc.is_singleton v2 - && AliasTarget.use (PowLoc.min_elt v1) ret_loc - then ret_alias := Some (AliasTarget.replace (PowLoc.min_elt v2) ret_loc) - | None -> - () - in let add_pair_sym_main_value v1 v2 ~e2_opt l = Option.value_map (Val.get_sym_var v1) ~default:l ~f:(fun var -> let sym_exp_opt = @@ -548,20 +537,17 @@ let get_matching_pairs : (var, Relation.SymExp.of_sym s2) :: l ) in let add_pair_val v1 v2 ~e2_opt rel_pairs = - add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ; rel_pairs |> add_pair_sym_main_value v1 v2 ~e2_opt |> add_pair_sym (get_offset_sym v1) (get_offset_sym v2) |> add_pair_sym (get_size_sym v1) (get_size_sym v2) in let add_pair_field v1 v2 pairs fn = - add_ret_alias (append_field v1 fn) (append_field v2 fn) ; let v1' = deref_field v1 fn callee_exit_mem in let v2' = deref_field v2 fn caller_mem in add_pair_val v1' v2' ~e2_opt:None pairs in let add_pair_ptr typ v1 v2 pairs = - add_ret_alias (Val.get_all_locs v1) (Val.get_all_locs v2) ; match typ.Typ.desc with | Typ.Tptr ({desc= Tstruct typename}, _) -> ( match Tenv.lookup tenv typename with @@ -577,10 +563,7 @@ let get_matching_pairs : | _ -> pairs in - let rel_pairs = - [] |> add_pair_val callee_v actual ~e2_opt:actual_exp_opt |> add_pair_ptr typ callee_v actual - in - (!ret_alias, rel_pairs) + [] |> add_pair_val callee_v actual ~e2_opt:actual_exp_opt |> add_pair_ptr typ callee_v actual let subst_map_of_rel_pairs : @@ -612,23 +595,18 @@ let rec list_fold2_def : let get_subst_map : - Tenv.t - -> Procdesc.t - -> (Exp.t * 'a) list - -> Mem.astate - -> Mem.astate - -> AliasTarget.t option * Relation.SubstMap.t = + Tenv.t -> Procdesc.t -> (Exp.t * 'a) list -> Mem.astate -> Mem.astate -> Relation.SubstMap.t = fun tenv callee_pdesc params caller_mem callee_exit_mem -> - let add_pair (formal, typ) (actual, actual_exp) (ret_alias, rel_l) = + let add_pair (formal, typ) (actual, actual_exp) rel_l = let callee_v = Mem.find (Loc.of_pvar formal) callee_exit_mem in - let ret_alias', new_rel_matching = + let new_rel_matching = get_matching_pairs tenv callee_v actual actual_exp typ caller_mem callee_exit_mem in - (Option.first_some ret_alias ret_alias', List.rev_append new_rel_matching rel_l) + List.rev_append new_rel_matching rel_l in let formals = get_formals callee_pdesc in let actuals = List.map ~f:(fun (a, _) -> (eval a caller_mem, Some a)) params in - let ret_alias, rel_pairs = - list_fold2_def ~default:(Val.Itv.top, None) ~f:add_pair formals actuals ~init:(None, []) + let rel_pairs = + list_fold2_def ~default:(Val.Itv.top, None) ~f:add_pair formals actuals ~init:[] in - (ret_alias, subst_map_of_rel_pairs rel_pairs) + subst_map_of_rel_pairs rel_pairs diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index c4189bd8f..731b60b3d 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -57,7 +57,8 @@ module Exec = struct fun ~decl_local pname ~node_hash location loc typ ~length ?stride ~inst_num ~dimension mem -> let offset = Itv.zero in let size = Option.value_map ~default:Itv.top ~f:Itv.of_int_lit length in - let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension in + let path = Loc.get_path loc in + let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension ~path in let arr = Dom.Val.of_array_alloc allocsite ~stride ~offset ~size |> Dom.Val.add_trace_elem (Trace.ArrDecl location) @@ -83,7 +84,8 @@ module Exec = struct -> Dom.Mem.astate -> Dom.Mem.astate * int = fun pname ~node_hash location loc ~inst_num ~dimension mem -> - let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension in + let path = Loc.get_path loc in + let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension ~path in let alloc_loc = Loc.of_allocsite allocsite in let alist = Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) @@ -141,7 +143,9 @@ module Exec = struct in let alloc_num = Itv.Counter.next new_alloc_num in let elem = Trace.SymAssign (loc, location) in - let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num in + let allocsite = + Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num ~path:(Some path) + in let arr = Dom.Val.of_array_alloc allocsite ~stride:None ~offset ~size |> Dom.Val.add_trace_elem elem in @@ -149,9 +153,7 @@ module Exec = struct mem |> Dom.Mem.add_heap loc arr |> Dom.Mem.init_param_relation loc |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None in - let deref_loc = - Loc.of_allocsite (Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num) - in + let deref_loc = Loc.of_allocsite allocsite in let path = Itv.SymbolPath.index path in decl_sym_val pname path tenv ~node_hash location ~depth deref_loc typ mem @@ -174,7 +176,9 @@ module Exec = struct mem -> let alloc_num = Itv.Counter.next new_alloc_num in let elem = Trace.SymAssign (loc, location) in - let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num in + let allocsite = + Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num ~path:(Some path) + in let alloc_loc = Loc.of_allocsite allocsite in let v = Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) |> Dom.Val.add_trace_elem elem in let mem = Dom.Mem.add_heap loc v mem in @@ -199,8 +203,9 @@ module Exec = struct Dom.Mem.add_heap loc size mem - let init_array_fields tenv pname ~node_hash typ locs ?dyn_length mem = - let rec init_field locs dimension ?dyn_length (mem, inst_num) (field_name, field_typ, _) = + let init_array_fields tenv pname path ~node_hash typ locs ?dyn_length mem = + let rec init_field path locs dimension ?dyn_length (mem, inst_num) (field_name, field_typ, _) = + let field_path = Option.map path ~f:(fun path -> Symb.SymbolPath.field path field_name) in let field_loc = PowLoc.append_field locs ~fn:field_name in let mem = match field_typ.Typ.desc with @@ -212,28 +217,30 @@ module Exec = struct Itv.plus i length ) in let stride = Option.map stride ~f:IntLit.to_int_exn in - let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension in + let allocsite = + Allocsite.make pname ~node_hash ~inst_num ~dimension ~path:field_path + in let offset, size = (Itv.zero, length) in let v = Dom.Val.of_array_alloc allocsite ~stride ~offset ~size in mem |> Dom.Mem.strong_update field_loc v |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None | _ -> - init_fields field_typ field_loc dimension ?dyn_length mem + init_fields field_path field_typ field_loc dimension ?dyn_length mem in (mem, inst_num + 1) - and init_fields typ locs dimension ?dyn_length mem = + and init_fields path typ locs dimension ?dyn_length mem = match typ.Typ.desc with | Tstruct typename -> ( match Tenv.lookup tenv typename with | Some str -> - let f = init_field locs (dimension + 1) in + let f = init_field path locs (dimension + 1) in IList.fold_last ~f ~f_last:(f ?dyn_length) ~init:(mem, 1) str.Typ.Struct.fields |> fst | None -> mem ) | _ -> mem in - init_fields typ locs 1 ?dyn_length mem + init_fields path typ locs 1 ?dyn_length mem let rec set_dyn_length tenv typ locs dyn_length mem = diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index 4e199e06a..552c7affe 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -110,6 +110,7 @@ module Exec : sig val init_array_fields : Tenv.t -> Typ.Procname.t + -> Itv.SymbolPath.partial option -> node_hash:int -> Typ.t -> PowLoc.t diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index b25d73d79..4822d599b 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/infer/src/bufferoverrun/symb.mli @@ -17,6 +17,7 @@ end module SymbolPath : sig type partial = private Pvar of Pvar.t | Index of partial | Field of Typ.Fieldname.t * partial + [@@deriving compare] type t = private Normal of partial | Offset of partial | Length of partial