From 7d703106910b08fc753fd9a25d97c1ce1ca6a5ae Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Thu, 27 Apr 2017 04:50:03 -0700 Subject: [PATCH] [inferbo] Yack manucuring Reviewed By: jvillard Differential Revision: D4961957 fbshipit-source-id: 06b2e48 --- infer/src/bufferoverrun/absLoc.ml | 14 +------- .../src/bufferoverrun/bufferOverrunChecker.ml | 34 +++++++++---------- .../src/bufferoverrun/bufferOverrunDomain.ml | 4 +-- .../bufferoverrun/bufferOverrunSemantics.ml | 2 +- 4 files changed, 21 insertions(+), 33 deletions(-) diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 10265eef2..fc107271b 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -37,10 +37,6 @@ struct | Allocsite a -> Allocsite.pp fmt a | Field (l, f) -> F.fprintf fmt "%a.%a" pp l Fieldname.pp f let is_var = function Var _ -> true | _ -> false - let is_pvar_in_reg v = - Var.pp F.str_formatter v; - let s = F.flush_str_formatter () in - s.[0] = '&' let is_logical_var = function | Var (Var.LogicalVar _) -> true | _ -> false @@ -58,15 +54,7 @@ end module PowLoc = struct - include AbstractDomain.FiniteSet - (struct - include Set.Make (struct type t = Loc.t [@@deriving compare] end) - let pp_element fmt e = Loc.pp fmt e - let pp fmt s = - Format.fprintf fmt "{"; - iter (fun e -> Format.fprintf fmt "%a," pp_element e) s; - Format.fprintf fmt "}" - end) + include AbstractDomain.FiniteSet(PrettyPrintable.MakePPSet(Loc)) let bot = empty let is_bot = is_empty diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index b2140a644..b1dac2962 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -45,7 +45,7 @@ struct let model_malloc : Typ.Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node - -> Dom.Mem.t -> Dom.Mem.t + -> Dom.Mem.astate -> Dom.Mem.astate = fun pname ret params node mem -> match ret with | Some (id, _) -> @@ -66,24 +66,24 @@ struct let model_realloc : Typ.Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node - -> Dom.Mem.t -> Dom.Mem.t + -> Dom.Mem.astate -> Dom.Mem.astate = fun pname ret params node mem -> model_malloc pname ret (List.tl_exn params) node mem - let model_natual_itv : (Ident.t * Typ.t) option -> Dom.Mem.t -> Dom.Mem.t + let model_natual_itv : (Ident.t * Typ.t) option -> Dom.Mem.astate -> Dom.Mem.astate = fun ret mem -> match ret with | Some (id, _) -> Dom.Mem.add_stack (Loc.of_id id) Dom.Val.nat_itv mem | _ -> mem - let model_unknown_itv : (Ident.t * Typ.t) option -> Dom.Mem.t -> Dom.Mem.t + let model_unknown_itv : (Ident.t * Typ.t) option -> Dom.Mem.astate -> Dom.Mem.astate = fun ret mem -> match ret with Some (id, _) -> Dom.Mem.add_stack (Loc.of_id id) Dom.Val.top_itv mem | None -> mem let model_infer_print - : (Exp.t * Typ.t) list -> Dom.Mem.t -> Location.t -> Dom.Mem.t + : (Exp.t * Typ.t) list -> Dom.Mem.astate -> Location.t -> Dom.Mem.astate = fun params mem loc -> match params with | (e, _) :: _ -> @@ -97,8 +97,8 @@ struct let handle_unknown_call : Typ.Procname.t -> (Ident.t * Typ.t) option -> Typ.Procname.t - -> (Exp.t * Typ.t) list -> CFG.node -> Dom.Mem.t -> Location.t - -> Dom.Mem.t + -> (Exp.t * Typ.t) list -> CFG.node -> Dom.Mem.astate -> Location.t + -> Dom.Mem.astate = fun pname ret callee_pname params node mem loc -> match Typ.Procname.get_method callee_pname with | "malloc" @@ -175,7 +175,7 @@ struct | _ -> (mem, sym_num + 6) let declare_symbolic_parameter - : Procdesc.t -> Tenv.t -> CFG.node -> int -> Dom.Mem.t -> Dom.Mem.t + : Procdesc.t -> Tenv.t -> CFG.node -> int -> Dom.Mem.astate -> Dom.Mem.astate = fun pdesc tenv node inst_num mem -> let pname = Procdesc.get_proc_name pdesc in let add_formal (mem, inst_num, sym_num) (pvar, typ) = @@ -197,7 +197,7 @@ struct let instantiate_ret : Tenv.t -> Procdesc.t option -> Typ.Procname.t -> (Exp.t * Typ.t) list - -> Dom.Mem.t -> Dom.Summary.t -> Location.t -> Dom.Val.astate + -> Dom.Mem.astate -> Dom.Summary.t -> Location.t -> Dom.Val.astate = fun tenv callee_pdesc callee_pname params caller_mem summary loc -> let callee_entry_mem = Dom.Summary.get_input summary in let callee_exit_mem = Dom.Summary.get_output summary in @@ -212,7 +212,7 @@ struct |> Dom.Val.normalize (* normalize bottom *) | _ -> Dom.Val.bot - let print_debug_info : Sil.instr -> Dom.Mem.t -> Dom.Mem.t -> unit + let print_debug_info : Sil.instr -> Dom.Mem.astate -> Dom.Mem.astate -> unit = fun instr pre post -> if Config.bo_debug >= 2 then begin @@ -229,13 +229,13 @@ struct end let exec_instr - : Dom.Mem.t -> extras ProcData.t -> CFG.node -> Sil.instr -> Dom.Mem.astate + : Dom.Mem.astate -> extras ProcData.t -> CFG.node -> Sil.instr -> Dom.Mem.astate = fun mem { pdesc; tenv; extras } node instr -> let pname = Procdesc.get_proc_name pdesc in let try_decl_arr (mem, inst_num) (pvar, typ) = match typ.Typ.desc with | Typ.Tarray (typ, Some len) -> - let loc = Loc.of_var (Var.of_pvar pvar) in + let loc = Loc.of_pvar pvar in let mem = declare_array pname node loc typ len ~inst_num ~dimension:1 mem in @@ -328,7 +328,7 @@ struct let instantiate_cond : Tenv.t -> Typ.Procname.t -> Procdesc.t option -> (Exp.t * Typ.t) list - -> Dom.Mem.t -> Summary.payload -> Location.t -> Dom.ConditionSet.t + -> Dom.Mem.astate -> Summary.payload -> Location.t -> Dom.ConditionSet.t = fun tenv caller_pname callee_pdesc params caller_mem summary loc -> let callee_entry_mem = Dom.Summary.get_input summary in let callee_cond = Dom.Summary.get_cond_set summary in @@ -341,7 +341,7 @@ struct Dom.ConditionSet.subst callee_cond subst_map caller_pname pname loc | _ -> callee_cond - let print_debug_info : Sil.instr -> Dom.Mem.t -> Dom.ConditionSet.t -> unit + let print_debug_info : Sil.instr -> Dom.Mem.astate -> Dom.ConditionSet.t -> unit = fun instr pre cond_set -> if Config.bo_debug >= 2 then (F.fprintf F.err_formatter "@.@.================================@."; @@ -355,8 +355,8 @@ struct F.fprintf F.err_formatter "================================@.@.") let collect_instr - : extras ProcData.t -> CFG.node -> Dom.ConditionSet.t * Dom.Mem.t - -> Sil.instr -> Dom.ConditionSet.t * Dom.Mem.t + : extras ProcData.t -> CFG.node -> Dom.ConditionSet.t * Dom.Mem.astate + -> Sil.instr -> Dom.ConditionSet.t * Dom.Mem.astate = fun ({ pdesc; tenv; extras } as pdata) node (cond_set, mem) instr -> let pname = Procdesc.get_proc_name pdesc in let cond_set = @@ -379,7 +379,7 @@ struct (cond_set, mem) let collect_instrs - : extras ProcData.t -> CFG.node -> Sil.instr list -> Dom.Mem.t + : extras ProcData.t -> CFG.node -> Sil.instr list -> Dom.Mem.astate -> Dom.ConditionSet.t -> Dom.ConditionSet.t = fun pdata node instrs mem cond_set -> List.fold ~f:(collect_instr pdata node) ~init:(cond_set, mem) instrs diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 0783acc8e..a4dd8ddea 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -88,8 +88,8 @@ let filter1 : t -> bool let filter2 : t -> bool = fun c -> - (not (Itv.is_finite c.idx) || not (Itv.is_finite c.size)) (* basically, alarms involving infinify are filtered *) - && (* except the following cases : *) + (not (Itv.is_finite c.idx) || not (Itv.is_finite c.size)) (* basically, alarms involving infinity are filtered *) + && (* except the following cases: *) not ((Itv.Bound.is_not_infty (Itv.lb c.idx) && (* idx non-infty lb < 0 *) Itv.Bound.lt (Itv.lb c.idx) Itv.Bound.zero) || diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 27042d1e2..f3ddf107d 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -419,7 +419,7 @@ struct let new_matching = get_matching_pairs tenv formal actual typ caller_mem callee_entry_mem in - List.append new_matching l + List.rev_append new_matching l in let formals = get_formals callee_pdesc in let actuals = List.map ~f:(fun (a, _) -> eval a caller_mem loc) params in