From 0ec75c587f16e2f108a38a1f4dfc197651de6a05 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Mon, 26 Nov 2018 01:31:51 -0800 Subject: [PATCH] [inferbo] Minor simplifications Reviewed By: ezgicicek Differential Revision: D13190906 fbshipit-source-id: 0bb65fa30 --- .../src/bufferoverrun/bufferOverrunDomain.ml | 2 ++ .../src/bufferoverrun/bufferOverrunModels.ml | 6 ++--- .../bufferoverrun/bufferOverrunSemantics.ml | 25 +++++++++++-------- infer/src/bufferoverrun/bufferOverrunUtils.ml | 5 ++-- infer/src/istd/IOption.ml | 2 ++ infer/src/istd/IOption.mli | 3 +++ 6 files changed, 25 insertions(+), 18 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 89ace8ffe..d1905fd9a 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -343,6 +343,8 @@ module Val = struct else {v with arrayblk= ArrayBlk.set_stride new_stride v.arrayblk} + let unknown_locs = of_pow_loc PowLoc.unknown ~traces:TraceSet.empty + module Itv = struct let m1_255 = of_itv Itv.m1_255 diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 488219cf8..ebdae84b1 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -107,7 +107,7 @@ let malloc size_exp = let typ, stride, length0, dyn_length = get_malloc_info size_exp in let length = Sem.eval integer_type_widths length0 mem in let traces = Trace.(Set.add_elem location ArrayDeclaration) (Dom.Val.get_traces length) in - let path = Option.value_map (Dom.Mem.find_simple_alias id mem) ~default:None ~f:Loc.get_path in + let path = Option.bind (Dom.Mem.find_simple_alias id mem) ~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 = @@ -389,9 +389,7 @@ module Collection = struct let new_list _ = let exec {pname; node_hash; location} ~ret:(id, _) mem = let loc = Loc.of_id id in - let path = - Option.value_map (Dom.Mem.find_simple_alias id mem) ~default:None ~f:Loc.get_path - in + let path = Option.bind (Dom.Mem.find_simple_alias id mem) ~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 diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 40c2a66b2..bd26fcbe9 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -142,14 +142,14 @@ let set_array_stride integer_type_widths typ v = let rec eval : Typ.IntegerWidths.t -> Exp.t -> Mem.astate -> Val.t = fun integer_type_widths exp mem -> - if must_alias_cmp exp mem then Val.of_int 0 + if must_alias_cmp exp mem then Val.Itv.zero else match exp with | Exp.Var id -> Mem.find_stack (Var.of_id id |> Loc.of_var) mem | Exp.Lvar pvar -> - let ploc = Loc.of_pvar pvar in - if Mem.is_stack_loc ploc mem then Mem.find ploc mem else Val.of_loc ploc + let loc = Loc.of_pvar pvar in + if Mem.is_stack_loc loc mem then Mem.find loc mem else Val.of_loc loc | Exp.UnOp (uop, e, _) -> eval_unop integer_type_widths uop e mem | Exp.BinOp (bop, e1, e2) -> @@ -174,27 +174,30 @@ let rec eval : Typ.IntegerWidths.t -> Exp.t -> Mem.astate -> Val.t = and eval_lindex integer_type_widths array_exp index_exp mem = - let array_v, index_v = - (eval integer_type_widths array_exp mem, eval integer_type_widths index_exp mem) - in + let array_v = eval integer_type_widths array_exp mem in if ArrayBlk.is_bot (Val.get_array_blk array_v) then match array_exp with - | Exp.Lfield _ when not (PowLoc.is_bot (Val.get_pow_loc array_v)) -> - (* It handles the case accessing an array field of struct, + | Exp.Lfield _ -> + let array_locs = Val.get_pow_loc array_v in + if PowLoc.is_bot array_locs then Val.unknown_locs + else + (* It handles the case accessing an array field of struct, e.g., x.f[n] . Since our abstract domain distinguishes memory sections for each array fields in struct, it finds the memory section using the abstract memory, though the memory lookup is not required to evaluate the address of x.f[n] in the concrete semantics. *) - Val.plus_pi (Mem.find_set (Val.get_pow_loc array_v) mem) index_v + let index_v = eval integer_type_widths index_exp mem in + Val.plus_pi (Mem.find_set array_locs mem) index_v | _ -> - Val.of_pow_loc PowLoc.unknown ~traces:TraceSet.empty + Val.unknown_locs else match array_exp with | Exp.Lindex _ -> (* It handles multi-dimensional arrays. *) Mem.find_set (Val.get_all_locs array_v) mem | _ -> + let index_v = eval integer_type_widths index_exp mem in Val.plus_pi array_v index_v @@ -271,7 +274,7 @@ let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.astate -> Val.t = | Some (AliasTarget.Empty _) | None -> Val.bot ) | Exp.Lvar pvar -> - Mem.find_set (PowLoc.singleton (Loc.of_pvar pvar)) mem + Mem.find (Loc.of_pvar pvar) mem | Exp.BinOp (bop, e1, e2) -> eval_binop integer_type_widths bop e1 e2 mem | Exp.Cast (t, e) -> diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 98e8fd271..9eceb223d 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -146,13 +146,12 @@ module Exec = struct -> Dom.Mem.astate = fun ~decl_sym_val deref_kind pname symbol_table path tenv ~node_hash location ~depth loc typ ?offset ?size ?stride ~inst_num ~new_sym_num ~new_alloc_num mem -> - let option_value opt_x default_f = match opt_x with Some x -> x | None -> default_f () in let offset = - option_value offset (fun () -> + IOption.value_default_f offset ~f:(fun () -> Itv.make_sym pname symbol_table (Itv.SymbolPath.offset path) new_sym_num ) in let size = - option_value size (fun () -> + IOption.value_default_f size ~f:(fun () -> Itv.make_sym ~unsigned:true pname symbol_table (Itv.SymbolPath.length path) new_sym_num ) in diff --git a/infer/src/istd/IOption.ml b/infer/src/istd/IOption.ml index 782a56e4d..7ca0edbd1 100644 --- a/infer/src/istd/IOption.ml +++ b/infer/src/istd/IOption.ml @@ -8,3 +8,5 @@ open! IStd let find_value_exn = function None -> raise Caml.Not_found | Some v -> v + +let value_default_f ~f = function None -> f () | Some v -> v diff --git a/infer/src/istd/IOption.mli b/infer/src/istd/IOption.mli index 76d46b434..6c5177d37 100644 --- a/infer/src/istd/IOption.mli +++ b/infer/src/istd/IOption.mli @@ -9,3 +9,6 @@ open! IStd val find_value_exn : 'a option -> 'a (** Like [Option.value_exn] but raises [Caml.Not_found] when called with [None]. *) + +val value_default_f : f:(unit -> 'a) -> 'a option -> 'a +(** Like [Option.value ~default:(f ())] but [f] is called only if [None]. *)