diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml new file mode 100644 index 000000000..aad4a3274 --- /dev/null +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -0,0 +1,334 @@ +(* + * Copyright (c) 2016-present, Programming Research Laboratory (ROPAS) + * Seoul National University, Korea + * Copyright (c) 2017-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +open AbsLoc +open! AbstractDomain.Types +module BoUtils = BufferOverrunUtils +module Dom = BufferOverrunDomain +module L = Logging +module Models = BufferOverrunModels +module Sem = BufferOverrunSemantics + +module Payload = SummaryPayload.Make (struct + type t = BufferOverrunSummary.t + + let update_payloads astate (payloads : Payloads.t) = {payloads with buffer_overrun= Some astate} + + let of_payloads (payloads : Payloads.t) = payloads.buffer_overrun +end) + +type extras = {oenv: Dom.OndemandEnv.t} + +module CFG = ProcCfg.NormalOneInstrPerNode + +module Init = struct + let initial_state {ProcData.pdesc; tenv; extras= {oenv}} start_node = + let try_decl_local = + let pname = Procdesc.get_proc_name pdesc in + let model_env = + let node_hash = CFG.Node.hash start_node in + let location = CFG.Node.loc start_node in + let integer_type_widths = oenv.Dom.OndemandEnv.integer_type_widths in + BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths + in + fun (mem, inst_num) {ProcAttributes.name; typ} -> + let loc = Loc.of_pvar (Pvar.mk name pname) in + BoUtils.Exec.decl_local model_env (mem, inst_num) (loc, typ) + in + let mem = Dom.Mem.init oenv in + let mem, _ = List.fold ~f:try_decl_local ~init:(mem, 1) (Procdesc.get_locals pdesc) in + mem +end + +module TransferFunctions = struct + module CFG = CFG + module Domain = Dom.Mem + + type nonrec extras = extras + + let instantiate_mem_reachable (ret_id, _) callee_pdesc callee_pname ~callee_exit_mem + ({Dom.eval_locpath} as eval_sym_trace) mem location = + let formals = Procdesc.get_pvar_formals callee_pdesc in + let copy_reachable_locs_from locs mem = + let copy loc acc = + Option.value_map (Dom.Mem.find_opt loc callee_exit_mem) ~default:acc ~f:(fun v -> + let locs = PowLoc.subst_loc loc eval_locpath in + let v = Dom.Val.subst v eval_sym_trace location in + PowLoc.fold (fun loc acc -> Dom.Mem.add_heap loc v acc) locs acc ) + in + let reachable_locs = Dom.Mem.get_reachable_locs_from formals locs callee_exit_mem in + PowLoc.fold copy reachable_locs mem + in + let instantiate_ret_alias mem = + let subst_loc l = + Option.find_map (Loc.get_path l) ~f:(fun partial -> + try + let locs = eval_locpath partial in + match PowLoc.is_singleton_or_more locs with + | IContainer.Singleton loc -> + Some loc + | _ -> + 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 ret_id l mem) + in + let ret_var = Loc.of_var (Var.of_id ret_id) in + let ret_val = Dom.Mem.find (Loc.of_pvar (Pvar.get_ret_pvar callee_pname)) callee_exit_mem in + let formal_locs = + List.fold formals ~init:PowLoc.bot ~f:(fun acc (formal, _) -> + let v = Dom.Mem.find (Loc.of_pvar formal) callee_exit_mem in + PowLoc.join acc (Dom.Val.get_all_locs v) ) + in + Dom.Mem.add_stack ret_var (Dom.Val.subst ret_val eval_sym_trace location) mem + |> instantiate_ret_alias + |> copy_reachable_locs_from (PowLoc.join formal_locs (Dom.Val.get_all_locs ret_val)) + + + let forget_ret_relation ret callee_pname mem = + let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in + let ret_var = Loc.of_var (Var.of_id (fst ret)) in + Dom.Mem.forget_locs (PowLoc.add ret_loc (PowLoc.singleton ret_var)) mem + + + let is_external pname = + match pname with + | Typ.Procname.Java java_pname -> + Typ.Procname.Java.is_external java_pname + | _ -> + false + + + let instantiate_mem : + Tenv.t + -> Typ.IntegerWidths.t + -> Ident.t * Typ.t + -> Procdesc.t + -> Typ.Procname.t + -> (Exp.t * Typ.t) list + -> Dom.Mem.t + -> BufferOverrunSummary.memory + -> Location.t + -> Dom.Mem.t = + fun tenv integer_type_widths ret callee_pdesc callee_pname params caller_mem callee_exit_mem + location -> + let rel_subst_map = + Sem.get_subst_map tenv integer_type_widths callee_pdesc params caller_mem callee_exit_mem + in + let eval_sym_trace = + Sem.mk_eval_sym_trace integer_type_widths callee_pdesc params caller_mem ~strict:false + in + let caller_mem = + instantiate_mem_reachable ret callee_pdesc callee_pname ~callee_exit_mem eval_sym_trace + caller_mem location + |> forget_ret_relation ret callee_pname + in + Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem ~callee:callee_exit_mem + + + let exec_instr : Dom.Mem.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.t = + fun mem {pdesc; tenv; extras= {oenv= {integer_type_widths}}} node instr -> + match instr with + | Load (id, _, _, _) when Ident.is_none id -> + mem + | Load (id, Exp.Lvar pvar, _, location) when Pvar.is_compile_constant pvar || Pvar.is_ice pvar + -> ( + match Pvar.get_initializer_pname pvar with + | Some callee_pname -> ( + match + Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname + |> Option.bind ~f:Payload.of_summary + |> Option.map ~f:BufferOverrunSummary.get_output + with + | Some callee_mem -> + let v = Dom.Mem.find (Loc.of_pvar pvar) callee_mem in + Dom.Mem.add_stack (Loc.of_id id) v mem + | None -> + L.d_printfln_escaped "/!\\ Unknown initializer of global constant %a" (Pvar.pp Pp.text) + pvar ; + Dom.Mem.add_unknown_from id ~callee_pname ~location mem ) + | None -> + L.d_printfln_escaped "/!\\ Failed to get initializer name of global constant %a" + (Pvar.pp Pp.text) pvar ; + Dom.Mem.add_unknown id ~location mem ) + | Load (id, exp, _, _) -> + BoUtils.Exec.load_locs id (Sem.eval_locs exp mem) mem + | Store (exp1, _, Const (Const.Cstr s), location) -> + let locs = Sem.eval_locs exp1 mem in + let model_env = + let pname = Procdesc.get_proc_name pdesc in + let node_hash = CFG.Node.hash node in + BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths + in + let do_alloc = not (Sem.is_stack_exp exp1 mem) in + BoUtils.Exec.decl_string model_env ~do_alloc locs s mem + | Store (exp1, typ, exp2, location) -> + let locs = Sem.eval_locs exp1 mem in + let v = + Sem.eval integer_type_widths exp2 mem |> Dom.Val.add_assign_trace_elem location locs + in + let mem = + let sym_exps = + Dom.Relation.SymExp.of_exps + ~get_int_sym_f:(Sem.get_sym_f integer_type_widths mem) + ~get_offset_sym_f:(Sem.get_offset_sym_f integer_type_widths mem) + ~get_size_sym_f:(Sem.get_size_sym_f integer_type_widths mem) + exp2 + in + Dom.Mem.store_relation locs sym_exps mem + in + let mem = Dom.Mem.update_mem locs v mem in + let mem = + if Language.curr_language_is Clang && Typ.is_char typ then + BoUtils.Exec.set_c_strlen ~tgt:(Sem.eval integer_type_widths exp1 mem) ~src:v mem + else mem + in + let mem = + if not v.represents_multiple_values then + match PowLoc.is_singleton_or_more locs with + | IContainer.Singleton loc_v -> ( + let pname = Procdesc.get_proc_name pdesc in + match Typ.Procname.get_method pname with + | "__inferbo_empty" when Loc.is_return loc_v -> ( + match Procdesc.get_pvar_formals pdesc with + | [(formal, _)] -> + let formal_v = Dom.Mem.find (Loc.of_pvar formal) mem in + Dom.Mem.store_empty_alias formal_v loc_v mem + | _ -> + assert false ) + | _ -> + Dom.Mem.store_simple_alias loc_v exp2 mem ) + | _ -> + mem + else mem + 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 + | Call (((id, ret_typ) as ret), Const (Cfun callee_pname), params, location, _) -> ( + let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in + match Models.Call.dispatch tenv callee_pname params with + | Some {Models.exec} -> + let model_env = + let node_hash = CFG.Node.hash node in + BoUtils.ModelEnv.mk_model_env callee_pname ~node_hash location tenv + integer_type_widths + in + exec model_env ~ret mem + | None -> ( + match + Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname + |> Option.bind ~f:(fun callee_summary -> + Payload.of_summary callee_summary + |> Option.map ~f:(fun payload -> + ( BufferOverrunSummary.get_output payload + , Summary.get_proc_desc callee_summary ) ) ) + with + | Some (callee_exit_mem, callee_pdesc) -> + instantiate_mem tenv integer_type_widths ret callee_pdesc callee_pname params mem + callee_exit_mem location + | None -> + (* This may happen for procedures with a biabduction model too. *) + L.d_printfln_escaped "/!\\ Unknown call to %a" Typ.Procname.pp callee_pname ; + if is_external callee_pname then ( + L.(debug BufferOverrun Verbose) + "/!\\ External call to unknown %a \n\n" Typ.Procname.pp callee_pname ; + let callsite = CallSite.make callee_pname location in + let path = Symb.SymbolPath.of_callsite ~ret_typ callsite in + let loc = Loc.of_allocsite (Allocsite.make_symbol path) in + let v = Dom.Mem.find loc mem in + Dom.Mem.add_stack (Loc.of_id id) v mem ) + else Dom.Mem.add_unknown_from id ~callee_pname ~location mem ) ) + | Call ((id, _), fun_exp, _, location, _) -> + let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in + L.d_printfln_escaped "/!\\ Call to non-const function %a" Exp.pp fun_exp ; + Dom.Mem.add_unknown id ~location mem + | ExitScope (dead_vars, _) -> + Dom.Mem.remove_temps (List.filter_map dead_vars ~f:Var.get_ident) mem + | Abstract _ | Nullify _ -> + mem + + + let pp_session_name node fmt = F.fprintf fmt "bufferoverrun %a" CFG.Node.pp_id (CFG.Node.id node) +end + +module Analyzer = AbstractInterpreter.MakeWTO (TransferFunctions) + +type invariant_map = Analyzer.invariant_map + +type local_decls = PowLoc.t + +type memory_summary = BufferOverrunSummary.memory + +let extract_pre = Analyzer.extract_pre + +let extract_post = Analyzer.extract_post + +let extract_state = Analyzer.extract_state + +let get_local_decls : Procdesc.t -> local_decls = + fun proc_desc -> + let proc_name = Procdesc.get_proc_name proc_desc in + let accum_local_decls acc {ProcAttributes.name} = + let pvar = Pvar.mk name proc_name in + let loc = Loc.of_pvar pvar in + PowLoc.add loc acc + in + Procdesc.get_locals proc_desc |> List.fold ~init:PowLoc.empty ~f:accum_local_decls + + +let cached_compute_invariant_map = + let compute_invariant_map : Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> invariant_map = + fun pdesc tenv integer_type_widths -> + Preanal.do_preanalysis pdesc tenv ; + let cfg = CFG.from_pdesc pdesc in + let pdata = + let oenv = Dom.OndemandEnv.mk pdesc tenv integer_type_widths in + ProcData.make pdesc tenv {oenv} + in + let initial = Init.initial_state pdata (CFG.start_node cfg) in + Analyzer.exec_pdesc ~do_narrowing:true ~initial pdata + in + (* Use a weak Hashtbl to prevent memory leaks (GC unnecessarily keeps invariant maps around) *) + let module WeakInvMapHashTbl = Caml.Weak.Make (struct + type t = Typ.Procname.t * invariant_map option + + let equal (pname1, _) (pname2, _) = Typ.Procname.equal pname1 pname2 + + let hash (pname, _) = Hashtbl.hash pname + end) in + let inv_map_cache = WeakInvMapHashTbl.create 100 in + fun pdesc tenv integer_type_widths -> + let pname = Procdesc.get_proc_name pdesc in + match WeakInvMapHashTbl.find_opt inv_map_cache (pname, None) with + | Some (_, Some inv_map) -> + inv_map + | Some (_, None) -> + (* this should never happen *) + assert false + | None -> + let inv_map = compute_invariant_map pdesc tenv integer_type_widths in + WeakInvMapHashTbl.add inv_map_cache (pname, Some inv_map) ; + inv_map + + +let compute_summary : local_decls -> CFG.t -> invariant_map -> memory_summary = + fun locals cfg inv_map -> + let exit_node_id = CFG.exit_node cfg |> CFG.Node.id in + match extract_post exit_node_id inv_map with + | Some exit_mem -> + exit_mem |> Dom.Mem.forget_locs locals |> Dom.Mem.unset_oenv + | None -> + Bottom diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.mli b/infer/src/bufferoverrun/bufferOverrunAnalysis.mli new file mode 100644 index 000000000..81bd559f3 --- /dev/null +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.mli @@ -0,0 +1,28 @@ +(* + * Copyright (c) 2017-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +module CFG = ProcCfg.NormalOneInstrPerNode + +module Payload : SummaryPayload.S with type t = BufferOverrunSummary.t + +type invariant_map + +type local_decls = AbsLoc.PowLoc.t + +val cached_compute_invariant_map : Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> invariant_map + +val compute_summary : local_decls -> CFG.t -> invariant_map -> BufferOverrunSummary.memory + +val extract_pre : CFG.Node.id -> invariant_map -> BufferOverrunDomain.Mem.t option + +val extract_post : CFG.Node.id -> invariant_map -> BufferOverrunDomain.Mem.t option + +val extract_state : + CFG.Node.id -> invariant_map -> BufferOverrunDomain.Mem.t AbstractInterpreter.State.t option + +val get_local_decls : Procdesc.t -> local_decls diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 6b3c1648a..fdabd1ad5 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -11,742 +11,416 @@ open! IStd open AbsLoc open! AbstractDomain.Types module BoUtils = BufferOverrunUtils +module CFG = BufferOverrunAnalysis.CFG module Dom = BufferOverrunDomain -module Relation = BufferOverrunDomainRelation module L = Logging module Models = BufferOverrunModels +module PO = BufferOverrunProofObligations +module Relation = BufferOverrunDomainRelation module Sem = BufferOverrunSemantics module Trace = BufferOverrunTrace -module Payload = SummaryPayload.Make (struct - type t = BufferOverrunSummary.t - - let update_payloads astate (payloads : Payloads.t) = {payloads with buffer_overrun= Some astate} - - let of_payloads (payloads : Payloads.t) = payloads.buffer_overrun -end) - -type extras = Dom.OndemandEnv.t - -module CFG = ProcCfg.NormalOneInstrPerNode +module UnusedBranch = struct + type t = {node: CFG.Node.t; location: Location.t; condition: Exp.t; true_branch: bool} -module Init = struct - let initial_state {ProcData.pdesc; tenv; extras= oenv} start_node = - let try_decl_local = - let pname = Procdesc.get_proc_name pdesc in - let model_env = - let node_hash = CFG.Node.hash start_node in - let location = CFG.Node.loc start_node in - let integer_type_widths = oenv.Dom.OndemandEnv.integer_type_widths in - BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths + let report tenv summary {node; location; condition; true_branch} = + let desc = + let err_desc = + let i = match condition with Exp.Const (Const.Cint i) -> i | _ -> IntLit.zero in + Errdesc.explain_condition_always_true_false tenv i condition + (CFG.Node.underlying_node node) location in - fun (mem, inst_num) {ProcAttributes.name; typ} -> - let loc = Loc.of_pvar (Pvar.mk name pname) in - BoUtils.Exec.decl_local model_env (mem, inst_num) (loc, typ) - in - let mem = Dom.Mem.init oenv in - let mem, _ = List.fold ~f:try_decl_local ~init:(mem, 1) (Procdesc.get_locals pdesc) in - mem -end - -module TransferFunctions = struct - module CFG = CFG - module Domain = Dom.Mem - - type nonrec extras = extras - - let instantiate_mem_reachable (ret_id, _) callee_pdesc callee_pname ~callee_exit_mem - ({Dom.eval_locpath} as eval_sym_trace) mem location = - let formals = Procdesc.get_pvar_formals callee_pdesc in - let copy_reachable_locs_from locs mem = - let copy loc acc = - Option.value_map (Dom.Mem.find_opt loc callee_exit_mem) ~default:acc ~f:(fun v -> - let locs = PowLoc.subst_loc loc eval_locpath in - let v = Dom.Val.subst v eval_sym_trace location in - PowLoc.fold (fun loc acc -> Dom.Mem.add_heap loc v acc) locs acc ) - in - let reachable_locs = Dom.Mem.get_reachable_locs_from formals locs callee_exit_mem in - PowLoc.fold copy reachable_locs mem - in - let instantiate_ret_alias mem = - let subst_loc l = - Option.find_map (Loc.get_path l) ~f:(fun partial -> - try - let locs = eval_locpath partial in - match PowLoc.is_singleton_or_more locs with - | IContainer.Singleton loc -> - Some loc - | _ -> - 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 ret_id l mem) - in - let ret_var = Loc.of_var (Var.of_id ret_id) in - let ret_val = Dom.Mem.find (Loc.of_pvar (Pvar.get_ret_pvar callee_pname)) callee_exit_mem in - let formal_locs = - List.fold formals ~init:PowLoc.bot ~f:(fun acc (formal, _) -> - let v = Dom.Mem.find (Loc.of_pvar formal) callee_exit_mem in - PowLoc.join acc (Dom.Val.get_all_locs v) ) - in - Dom.Mem.add_stack ret_var (Dom.Val.subst ret_val eval_sym_trace location) mem - |> instantiate_ret_alias - |> copy_reachable_locs_from (PowLoc.join formal_locs (Dom.Val.get_all_locs ret_val)) - - - let forget_ret_relation ret callee_pname mem = - let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar callee_pname) in - let ret_var = Loc.of_var (Var.of_id (fst ret)) in - Dom.Mem.forget_locs (PowLoc.add ret_loc (PowLoc.singleton ret_var)) mem - - - let is_external pname = - match pname with - | Typ.Procname.Java java_pname -> - Typ.Procname.Java.is_external java_pname - | _ -> - false - - - let instantiate_mem : - Tenv.t - -> Typ.IntegerWidths.t - -> Ident.t * Typ.t - -> Procdesc.t - -> Typ.Procname.t - -> (Exp.t * Typ.t) list - -> Dom.Mem.t - -> BufferOverrunSummary.t - -> Location.t - -> Dom.Mem.t = - fun tenv integer_type_widths ret callee_pdesc callee_pname params caller_mem summary location -> - let callee_exit_mem = BufferOverrunSummary.get_output summary in - let rel_subst_map = - Sem.get_subst_map tenv integer_type_widths callee_pdesc params caller_mem callee_exit_mem - in - let eval_sym_trace = - Sem.mk_eval_sym_trace integer_type_widths callee_pdesc params caller_mem ~strict:false + F.asprintf "%a" Localise.pp_error_desc err_desc in - let caller_mem = - instantiate_mem_reachable ret callee_pdesc callee_pname ~callee_exit_mem eval_sym_trace - caller_mem location - |> forget_ret_relation ret callee_pname + let issue_type = + if true_branch then IssueType.condition_always_false else IssueType.condition_always_true in - Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem ~callee:callee_exit_mem - - - let exec_instr : Dom.Mem.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.t = - fun mem {pdesc; tenv; extras= {integer_type_widths}} node instr -> - match instr with - | Load (id, _, _, _) when Ident.is_none id -> - mem - | Load (id, Exp.Lvar pvar, _, location) when Pvar.is_compile_constant pvar || Pvar.is_ice pvar - -> ( - match Pvar.get_initializer_pname pvar with - | Some callee_pname -> ( - match Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname with - | Some callee_summary -> ( - match Payload.of_summary callee_summary with - | Some payload -> - let callee_mem = BufferOverrunSummary.get_output payload in - let v = Dom.Mem.find (Loc.of_pvar pvar) callee_mem in - Dom.Mem.add_stack (Loc.of_id id) v mem - | None -> - L.d_printfln_escaped "/!\\ Initializer of global constant %a has no inferbo payload" - (Pvar.pp Pp.text) pvar ; - Dom.Mem.add_unknown_from id ~callee_pname ~location mem ) - | None -> - L.d_printfln_escaped "/!\\ Unknown initializer of global constant %a" (Pvar.pp Pp.text) - pvar ; - Dom.Mem.add_unknown_from id ~callee_pname ~location mem ) - | None -> - L.d_printfln_escaped "/!\\ Failed to get initializer name of global constant %a" - (Pvar.pp Pp.text) pvar ; - Dom.Mem.add_unknown id ~location mem ) - | Load (id, exp, _, _) -> - BoUtils.Exec.load_locs id (Sem.eval_locs exp mem) mem - | Store (exp1, _, Const (Const.Cstr s), location) -> - let locs = Sem.eval_locs exp1 mem in - let model_env = - let pname = Procdesc.get_proc_name pdesc in - let node_hash = CFG.Node.hash node in - BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths - in - let do_alloc = not (Sem.is_stack_exp exp1 mem) in - BoUtils.Exec.decl_string model_env ~do_alloc locs s mem - | Store (exp1, typ, exp2, location) -> - let locs = Sem.eval_locs exp1 mem in - let v = - Sem.eval integer_type_widths exp2 mem |> Dom.Val.add_assign_trace_elem location locs - in - let mem = - let sym_exps = - Dom.Relation.SymExp.of_exps - ~get_int_sym_f:(Sem.get_sym_f integer_type_widths mem) - ~get_offset_sym_f:(Sem.get_offset_sym_f integer_type_widths mem) - ~get_size_sym_f:(Sem.get_size_sym_f integer_type_widths mem) - exp2 - in - Dom.Mem.store_relation locs sym_exps mem - in - let mem = Dom.Mem.update_mem locs v mem in - let mem = - if Language.curr_language_is Clang && Typ.is_char typ then - BoUtils.Exec.set_c_strlen ~tgt:(Sem.eval integer_type_widths exp1 mem) ~src:v mem - else mem - in - let mem = - if not v.represents_multiple_values then - match PowLoc.is_singleton_or_more locs with - | IContainer.Singleton loc_v -> ( - let pname = Procdesc.get_proc_name pdesc in - match Typ.Procname.get_method pname with - | "__inferbo_empty" when Loc.is_return loc_v -> ( - match Procdesc.get_pvar_formals pdesc with - | [(formal, _)] -> - let formal_v = Dom.Mem.find (Loc.of_pvar formal) mem in - Dom.Mem.store_empty_alias formal_v loc_v mem - | _ -> - assert false ) - | _ -> - Dom.Mem.store_simple_alias loc_v exp2 mem ) - | _ -> - mem - else mem - 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 - | Call (((id, ret_typ) as ret), Const (Cfun callee_pname), params, location, _) -> ( - let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in - match Models.Call.dispatch tenv callee_pname params with - | Some {Models.exec} -> - let model_env = - let node_hash = CFG.Node.hash node in - BoUtils.ModelEnv.mk_model_env callee_pname ~node_hash location tenv - integer_type_widths - in - exec model_env ~ret mem - | None -> ( - match Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname with - | Some callee_summary -> ( - match Payload.of_summary callee_summary with - | Some payload -> - let callee_pdesc = Summary.get_proc_desc callee_summary in - instantiate_mem tenv integer_type_widths ret callee_pdesc callee_pname params mem - payload location - | None -> - (* This may happen for procedures with a biabduction model. *) - L.d_printfln_escaped "/!\\ Call to %a has no inferbo payload" Typ.Procname.pp - callee_pname ; - Dom.Mem.add_unknown_from id ~callee_pname ~location mem ) - | None -> - L.d_printfln_escaped "/!\\ Unknown call to %a" Typ.Procname.pp callee_pname ; - if is_external callee_pname then ( - L.(debug BufferOverrun Verbose) - "/!\\ External call to unknown %a \n\n" Typ.Procname.pp callee_pname ; - let callsite = CallSite.make callee_pname location in - let path = Symb.SymbolPath.of_callsite ~ret_typ callsite in - let loc = Loc.of_allocsite (Allocsite.make_symbol path) in - let v = Dom.Mem.find loc mem in - Dom.Mem.add_stack (Loc.of_id id) v mem ) - else Dom.Mem.add_unknown_from id ~callee_pname ~location mem ) ) - | Call ((id, _), fun_exp, _, location, _) -> - let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in - L.d_printfln_escaped "/!\\ Call to non-const function %a" Exp.pp fun_exp ; - Dom.Mem.add_unknown id ~location mem - | ExitScope (dead_vars, _) -> - Dom.Mem.remove_temps (List.filter_map dead_vars ~f:Var.get_ident) mem - | Abstract _ | Nullify _ -> - mem - - - let pp_session_name node fmt = F.fprintf fmt "bufferoverrun %a" CFG.Node.pp_id (CFG.Node.id node) + let ltr = [Errlog.make_trace_element 0 location "Here" []] in + Reporting.log_warning summary ~loc:location ~ltr issue_type desc end -module Analyzer = AbstractInterpreter.MakeWTO (TransferFunctions) - -type invariant_map = Analyzer.invariant_map - -module Report = struct - module UnusedBranch = struct - type t = {node: CFG.Node.t; location: Location.t; condition: Exp.t; true_branch: bool} - - let report tenv summary {node; location; condition; true_branch} = - let desc = - let err_desc = - let i = match condition with Exp.Const (Const.Cint i) -> i | _ -> IntLit.zero in - Errdesc.explain_condition_always_true_false tenv i condition - (CFG.Node.underlying_node node) location - in - F.asprintf "%a" Localise.pp_error_desc err_desc - in - let issue_type = - if true_branch then IssueType.condition_always_false else IssueType.condition_always_true - in - let ltr = [Errlog.make_trace_element 0 location "Here" []] in - Reporting.log_warning summary ~loc:location ~ltr issue_type desc - end - - module UnusedBranches = struct - type t = UnusedBranch.t list - - let empty = [] +module UnusedBranches = struct + type t = UnusedBranch.t list - let report tenv summary unused_branches = - List.iter unused_branches ~f:(UnusedBranch.report tenv summary) - end + let empty = [] - module UnreachableStatement = struct - type t = {location: Location.t} + let report tenv summary unused_branches = + List.iter unused_branches ~f:(UnusedBranch.report tenv summary) +end - let report summary {location} = - let ltr = [Errlog.make_trace_element 0 location "Here" []] in - Reporting.log_error summary ~loc:location ~ltr IssueType.unreachable_code_after - "Unreachable code after statement" - end +module UnreachableStatement = struct + type t = {location: Location.t} - module UnreachableStatements = struct - type t = UnreachableStatement.t list + let report summary {location} = + let ltr = [Errlog.make_trace_element 0 location "Here" []] in + Reporting.log_error summary ~loc:location ~ltr IssueType.unreachable_code_after + "Unreachable code after statement" +end - let empty = [] +module UnreachableStatements = struct + type t = UnreachableStatement.t list - let report summary unreachable_statements = - List.iter unreachable_statements ~f:(UnreachableStatement.report summary) - end + let empty = [] - module PO = BufferOverrunProofObligations + let report summary unreachable_statements = + List.iter unreachable_statements ~f:(UnreachableStatement.report summary) +end - module Checks = struct - type t = - { cond_set: PO.ConditionSet.checked_t - ; unused_branches: UnusedBranches.t - ; unreachable_statements: UnreachableStatements.t } +module Checks = struct + type t = + { cond_set: PO.ConditionSet.checked_t + ; unused_branches: UnusedBranches.t + ; unreachable_statements: UnreachableStatements.t } - let empty = - { cond_set= PO.ConditionSet.empty - ; unused_branches= UnusedBranches.empty - ; unreachable_statements= UnreachableStatements.empty } - end + let empty = + { cond_set= PO.ConditionSet.empty + ; unused_branches= UnusedBranches.empty + ; unreachable_statements= UnreachableStatements.empty } +end - module ExitStatement = struct - (* check that we are the last significant instruction +module ExitStatement = struct + (* check that we are the last significant instruction * of a procedure (no more significant instruction) * or of a block (goes directly to a node with multiple predecessors) *) - let rec is_end_of_block_or_procedure (cfg : CFG.t) node rem_instrs = - Instrs.for_all rem_instrs ~f:Sil.instr_is_auxiliary - && - match IContainer.singleton_or_more node ~fold:(CFG.fold_succs cfg) with - | IContainer.Empty -> - true - | Singleton succ -> - (* [succ] is a join, i.e. [node] is the end of a block *) - IContainer.mem_nth succ 1 ~fold:(CFG.fold_preds cfg) - || is_end_of_block_or_procedure cfg succ (CFG.instrs succ) - | More -> - false - end - - let add_unreachable_code (cfg : CFG.t) (node : CFG.Node.t) instr rem_instrs (checks : Checks.t) = - match instr with - | Sil.Prune (_, _, _, (Ik_land_lor | Ik_bexp)) -> - checks - | Sil.Prune (condition, location, true_branch, _) -> - let unused_branch = UnusedBranch.{node; location; condition; true_branch} in - {checks with unused_branches= unused_branch :: checks.unused_branches} - (* special case for `exit` when we're at the end of a block / procedure *) - | Sil.Call (_, Const (Cfun pname), _, _, _) - when String.equal (Typ.Procname.get_method pname) "exit" - && ExitStatement.is_end_of_block_or_procedure cfg node rem_instrs -> - checks - | _ -> - let location = Sil.instr_get_loc instr in - let unreachable_statement = UnreachableStatement.{location} in - {checks with unreachable_statements= unreachable_statement :: checks.unreachable_statements} - - - let check_binop_array_access : - Typ.IntegerWidths.t - -> is_plus:bool - -> e1:Exp.t - -> e2:Exp.t - -> Location.t - -> Dom.Mem.t - -> PO.ConditionSet.checked_t - -> PO.ConditionSet.checked_t = - fun integer_type_widths ~is_plus ~e1 ~e2 location mem cond_set -> - let arr = Sem.eval integer_type_widths e1 mem in - let idx = Sem.eval integer_type_widths e2 mem in - let idx_sym_exp = - Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) e2 - in - let relation = Dom.Mem.get_relation mem in - let latest_prune = Dom.Mem.get_latest_prune mem in - BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus ~last_included:false - ~latest_prune location cond_set - - - let check_binop : - Typ.IntegerWidths.t - -> bop:Binop.t - -> e1:Exp.t - -> e2:Exp.t - -> Location.t - -> Dom.Mem.t - -> PO.ConditionSet.checked_t - -> PO.ConditionSet.checked_t = - fun integer_type_widths ~bop ~e1 ~e2 location mem cond_set -> - match bop with - | Binop.PlusPI -> - check_binop_array_access integer_type_widths ~is_plus:true ~e1 ~e2 location mem cond_set - | Binop.MinusPI -> - check_binop_array_access integer_type_widths ~is_plus:false ~e1 ~e2 location mem cond_set - | _ -> - cond_set - - - let check_expr_for_array_access : - Typ.IntegerWidths.t - -> Exp.t - -> Location.t - -> Dom.Mem.t - -> PO.ConditionSet.checked_t - -> PO.ConditionSet.checked_t = - fun integer_type_widths exp location mem cond_set -> - let rec check_sub_expr exp cond_set = - match exp with - | Exp.Lindex (array_exp, index_exp) -> - cond_set |> check_sub_expr array_exp |> check_sub_expr index_exp - |> BoUtils.Check.lindex integer_type_widths ~array_exp ~index_exp ~last_included:false - mem location - | Exp.BinOp (_, e1, e2) -> - cond_set |> check_sub_expr e1 |> check_sub_expr e2 - | Exp.Lfield (e, _, _) | Exp.UnOp (_, e, _) | Exp.Exn e -> - check_sub_expr e cond_set - | Exp.Cast (_, e) -> - check_sub_expr e cond_set - | Exp.Closure {captured_vars} -> - List.fold captured_vars ~init:cond_set ~f:(fun cond_set (e, _, _) -> - check_sub_expr e cond_set ) - | Exp.Var _ | Exp.Lvar _ | Exp.Const _ | Exp.Sizeof _ -> - cond_set - in - let cond_set = check_sub_expr exp cond_set in - match exp with - | Exp.Var _ -> - let arr = Sem.eval integer_type_widths exp mem in - let idx, idx_sym_exp = (Dom.Val.Itv.zero, Some Relation.SymExp.zero) in - let relation = Dom.Mem.get_relation mem in - let latest_prune = Dom.Mem.get_latest_prune mem in - BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true - ~last_included:false ~latest_prune location cond_set - | Exp.BinOp (bop, e1, e2) -> - check_binop integer_type_widths ~bop ~e1 ~e2 location mem cond_set - | _ -> - cond_set - - - let check_binop_for_integer_overflow integer_type_widths bop ~lhs ~rhs location mem cond_set = - match bop with - | Binop.PlusA (Some _) | Binop.MinusA (Some _) | Binop.Mult (Some _) -> - let lhs_v = Sem.eval integer_type_widths lhs mem in - let rhs_v = Sem.eval integer_type_widths rhs mem in - let latest_prune = Dom.Mem.get_latest_prune mem in - BoUtils.Check.binary_operation integer_type_widths bop ~lhs:lhs_v ~rhs:rhs_v ~latest_prune - location cond_set - | _ -> - cond_set - + let rec is_end_of_block_or_procedure (cfg : CFG.t) node rem_instrs = + Instrs.for_all rem_instrs ~f:Sil.instr_is_auxiliary + && + match IContainer.singleton_or_more node ~fold:(CFG.fold_succs cfg) with + | IContainer.Empty -> + true + | Singleton succ -> + (* [succ] is a join, i.e. [node] is the end of a block *) + IContainer.mem_nth succ 1 ~fold:(CFG.fold_preds cfg) + || is_end_of_block_or_procedure cfg succ (CFG.instrs succ) + | More -> + false +end - let rec check_expr_for_integer_overflow integer_type_widths exp location mem cond_set = +let add_unreachable_code (cfg : CFG.t) (node : CFG.Node.t) instr rem_instrs (checks : Checks.t) = + match instr with + | Sil.Prune (_, _, _, (Ik_land_lor | Ik_bexp)) -> + checks + | Sil.Prune (condition, location, true_branch, _) -> + let unused_branch = UnusedBranch.{node; location; condition; true_branch} in + {checks with unused_branches= unused_branch :: checks.unused_branches} + (* special case for `exit` when we're at the end of a block / procedure *) + | Sil.Call (_, Const (Cfun pname), _, _, _) + when String.equal (Typ.Procname.get_method pname) "exit" + && ExitStatement.is_end_of_block_or_procedure cfg node rem_instrs -> + checks + | _ -> + let location = Sil.instr_get_loc instr in + let unreachable_statement = UnreachableStatement.{location} in + {checks with unreachable_statements= unreachable_statement :: checks.unreachable_statements} + + +let check_binop_array_access : + Typ.IntegerWidths.t + -> is_plus:bool + -> e1:Exp.t + -> e2:Exp.t + -> Location.t + -> Dom.Mem.t + -> PO.ConditionSet.checked_t + -> PO.ConditionSet.checked_t = + fun integer_type_widths ~is_plus ~e1 ~e2 location mem cond_set -> + let arr = Sem.eval integer_type_widths e1 mem in + let idx = Sem.eval integer_type_widths e2 mem in + let idx_sym_exp = Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) e2 in + let relation = Dom.Mem.get_relation mem in + let latest_prune = Dom.Mem.get_latest_prune mem in + BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus ~last_included:false + ~latest_prune location cond_set + + +let check_binop : + Typ.IntegerWidths.t + -> bop:Binop.t + -> e1:Exp.t + -> e2:Exp.t + -> Location.t + -> Dom.Mem.t + -> PO.ConditionSet.checked_t + -> PO.ConditionSet.checked_t = + fun integer_type_widths ~bop ~e1 ~e2 location mem cond_set -> + match bop with + | Binop.PlusPI -> + check_binop_array_access integer_type_widths ~is_plus:true ~e1 ~e2 location mem cond_set + | Binop.MinusPI -> + check_binop_array_access integer_type_widths ~is_plus:false ~e1 ~e2 location mem cond_set + | _ -> + cond_set + + +let check_expr_for_array_access : + Typ.IntegerWidths.t + -> Exp.t + -> Location.t + -> Dom.Mem.t + -> PO.ConditionSet.checked_t + -> PO.ConditionSet.checked_t = + fun integer_type_widths exp location mem cond_set -> + let rec check_sub_expr exp cond_set = match exp with - | Exp.UnOp (_, e, _) - | Exp.Exn e - | Exp.Lfield (e, _, _) - | Exp.Cast (_, e) - | Exp.Sizeof {dynamic_length= Some e} -> - check_expr_for_integer_overflow integer_type_widths e location mem cond_set - | Exp.BinOp (bop, lhs, rhs) -> - cond_set - |> check_binop_for_integer_overflow integer_type_widths bop ~lhs ~rhs location mem - |> check_expr_for_integer_overflow integer_type_widths lhs location mem - |> check_expr_for_integer_overflow integer_type_widths rhs location mem - | Exp.Lindex (e1, e2) -> - cond_set - |> check_expr_for_integer_overflow integer_type_widths e1 location mem - |> check_expr_for_integer_overflow integer_type_widths e2 location mem + | Exp.Lindex (array_exp, index_exp) -> + cond_set |> check_sub_expr array_exp |> check_sub_expr index_exp + |> BoUtils.Check.lindex integer_type_widths ~array_exp ~index_exp ~last_included:false mem + location + | Exp.BinOp (_, e1, e2) -> + cond_set |> check_sub_expr e1 |> check_sub_expr e2 + | Exp.Lfield (e, _, _) | Exp.UnOp (_, e, _) | Exp.Exn e -> + check_sub_expr e cond_set + | Exp.Cast (_, e) -> + check_sub_expr e cond_set | Exp.Closure {captured_vars} -> List.fold captured_vars ~init:cond_set ~f:(fun cond_set (e, _, _) -> - check_expr_for_integer_overflow integer_type_widths e location mem cond_set ) - | Exp.Var _ | Exp.Const _ | Exp.Lvar _ | Exp.Sizeof {dynamic_length= None} -> + check_sub_expr e cond_set ) + | Exp.Var _ | Exp.Lvar _ | Exp.Const _ | Exp.Sizeof _ -> cond_set - - - let instantiate_cond : - Tenv.t - -> Typ.IntegerWidths.t - -> Procdesc.t - -> (Exp.t * Typ.t) list - -> Dom.Mem.t - -> Payload.t - -> Location.t - -> PO.ConditionSet.checked_t = - fun tenv integer_type_widths callee_pdesc params caller_mem summary location -> - let callee_exit_mem = BufferOverrunSummary.get_output summary in - let callee_cond = BufferOverrunSummary.get_cond_set summary in - let rel_subst_map = - Sem.get_subst_map tenv integer_type_widths 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 integer_type_widths callee_pdesc params caller_mem - in - PO.ConditionSet.subst callee_cond eval_sym_trace rel_subst_map caller_rel pname location - - - let check_instr : - Procdesc.t - -> Tenv.t - -> Typ.IntegerWidths.t - -> CFG.Node.t - -> Sil.instr - -> Dom.Mem.t - -> PO.ConditionSet.checked_t - -> PO.ConditionSet.checked_t = - fun pdesc tenv integer_type_widths node instr mem cond_set -> - match instr with - | Sil.Load (_, exp, _, location) -> - cond_set - |> check_expr_for_array_access integer_type_widths exp location mem - |> check_expr_for_integer_overflow integer_type_widths exp location mem - | Sil.Store (lexp, _, rexp, location) -> - cond_set - |> check_expr_for_array_access integer_type_widths lexp location mem - |> check_expr_for_integer_overflow integer_type_widths lexp location mem - |> check_expr_for_integer_overflow integer_type_widths rexp location mem - | Sil.Call (_, Const (Cfun callee_pname), params, location, _) -> ( - let cond_set = - List.fold params ~init:cond_set ~f:(fun cond_set (exp, _) -> - check_expr_for_integer_overflow integer_type_widths exp location mem cond_set ) - in - match Models.Call.dispatch tenv callee_pname params with - | Some {Models.check} -> - let model_env = - let node_hash = CFG.Node.hash node in - let pname = Procdesc.get_proc_name pdesc in - BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths - in - check model_env mem cond_set - | None -> ( - match Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname with - | Some callee_summary -> ( - match Payload.of_summary callee_summary with - | Some callee_payload -> - let callee_pdesc = Summary.get_proc_desc callee_summary in - instantiate_cond tenv integer_type_widths callee_pdesc params mem callee_payload - location - |> PO.ConditionSet.join cond_set - | None -> - (* no inferbo payload *) cond_set ) - | None -> - (* unknown call *) cond_set ) ) - | Sil.Prune (exp, location, _, _) -> - check_expr_for_integer_overflow integer_type_widths exp location mem cond_set - | _ -> - cond_set - - - let print_debug_info : Sil.instr -> Dom.Mem.t -> PO.ConditionSet.checked_t -> unit = - fun instr pre cond_set -> - L.(debug BufferOverrun Verbose) "@\n@\n================================@\n" ; - L.(debug BufferOverrun Verbose) "@[Pre-state : @,%a" Dom.Mem.pp pre ; - L.(debug BufferOverrun Verbose) "@]@\n@\n%a" (Sil.pp_instr ~print_types:true Pp.text) instr ; - L.(debug BufferOverrun Verbose) "@\n@\n@[%a" PO.ConditionSet.pp cond_set ; - L.(debug BufferOverrun Verbose) "@]@\n" ; - L.(debug BufferOverrun Verbose) "================================@\n@." - - - let check_instrs : - Procdesc.t - -> Tenv.t - -> Typ.IntegerWidths.t - -> CFG.t - -> CFG.Node.t - -> Instrs.not_reversed_t - -> Dom.Mem.t AbstractInterpreter.State.t - -> Checks.t - -> Checks.t = - fun pdesc tenv integer_type_widths cfg node instrs state checks -> - match state with - | _ when Instrs.is_empty instrs -> - checks - | {AbstractInterpreter.State.pre= Bottom} -> - checks - | {AbstractInterpreter.State.pre= NonBottom _ as pre; post} -> - if Instrs.nth_exists instrs 1 then - L.(die InternalError) "Did not expect several instructions" ; - let instr = Instrs.nth_exn instrs 0 in - let checks = - match post with - | Bottom -> - add_unreachable_code cfg node instr Instrs.empty checks - | NonBottom _ -> - checks - in - let cond_set = check_instr pdesc tenv integer_type_widths node instr pre checks.cond_set in - print_debug_info instr pre cond_set ; - {checks with cond_set} - - - let check_node : - Procdesc.t - -> Tenv.t - -> Typ.IntegerWidths.t - -> CFG.t - -> invariant_map - -> Checks.t - -> CFG.Node.t - -> Checks.t = - fun pdesc tenv integer_type_widths cfg inv_map checks node -> - match Analyzer.extract_state (CFG.Node.id node) inv_map with - | Some state -> - let instrs = CFG.instrs node in - check_instrs pdesc tenv integer_type_widths cfg node instrs state checks - | _ -> - checks - - - let check_proc : - Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> CFG.t -> invariant_map -> Checks.t = - fun pdesc tenv integer_type_widths cfg inv_map -> - CFG.fold_nodes cfg - ~f:(check_node pdesc tenv integer_type_widths cfg inv_map) - ~init:Checks.empty - - - let report_errors : Tenv.t -> Summary.t -> Checks.t -> unit = - fun tenv summary {cond_set; unused_branches; unreachable_statements} -> - UnusedBranches.report tenv summary unused_branches ; - UnreachableStatements.report summary unreachable_statements ; - let report cond trace issue_type = - let location = PO.ConditionTrace.get_report_location trace in - let description ~markup = PO.description ~markup cond trace in - let trace = - let description = description ~markup:false in - Trace.Issue.make_err_trace ~description (PO.ConditionTrace.get_val_traces trace) - |> Errlog.concat_traces - in - Reporting.log_error summary ~loc:location ~ltr:trace issue_type (description ~markup:true) - in - PO.ConditionSet.report_errors ~report cond_set - - - let for_summary ~forget_locs - Checks.({ cond_set - ; unused_branches= _ (* intra-procedural *) - ; unreachable_statements= _ (* intra-procedural *) }) = - PO.ConditionSet.for_summary ~forget_locs cond_set -end - -type checks = Report.Checks.t - -type checks_summary = Report.PO.ConditionSet.summary_t - -type local_decls = PowLoc.t - -type memory_summary = BufferOverrunSummary.memory - -let extract_pre = Analyzer.extract_pre - -let extract_post = Analyzer.extract_post - -let get_local_decls : Procdesc.t -> local_decls = - fun proc_desc -> - let proc_name = Procdesc.get_proc_name proc_desc in - let accum_local_decls acc {ProcAttributes.name} = - let pvar = Pvar.mk name proc_name in - let loc = Loc.of_pvar pvar in - PowLoc.add loc acc in - Procdesc.get_locals proc_desc |> List.fold ~init:PowLoc.empty ~f:accum_local_decls - - -let cached_compute_invariant_map = - let compute_invariant_map : Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> invariant_map = - fun pdesc tenv integer_type_widths -> - Preanal.do_preanalysis pdesc tenv ; - let cfg = CFG.from_pdesc pdesc in - let pdata = - let oenv = Dom.OndemandEnv.mk pdesc tenv integer_type_widths in - ProcData.make pdesc tenv oenv - in - let initial = Init.initial_state pdata (CFG.start_node cfg) in - Analyzer.exec_pdesc ~do_narrowing:true ~initial pdata + let cond_set = check_sub_expr exp cond_set in + match exp with + | Exp.Var _ -> + let arr = Sem.eval integer_type_widths exp mem in + let idx, idx_sym_exp = (Dom.Val.Itv.zero, Some Relation.SymExp.zero) in + let relation = Dom.Mem.get_relation mem in + let latest_prune = Dom.Mem.get_latest_prune mem in + BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true + ~last_included:false ~latest_prune location cond_set + | Exp.BinOp (bop, e1, e2) -> + check_binop integer_type_widths ~bop ~e1 ~e2 location mem cond_set + | _ -> + cond_set + + +let check_binop_for_integer_overflow integer_type_widths bop ~lhs ~rhs location mem cond_set = + match bop with + | Binop.PlusA (Some _) | Binop.MinusA (Some _) | Binop.Mult (Some _) -> + let lhs_v = Sem.eval integer_type_widths lhs mem in + let rhs_v = Sem.eval integer_type_widths rhs mem in + let latest_prune = Dom.Mem.get_latest_prune mem in + BoUtils.Check.binary_operation integer_type_widths bop ~lhs:lhs_v ~rhs:rhs_v ~latest_prune + location cond_set + | _ -> + cond_set + + +let rec check_expr_for_integer_overflow integer_type_widths exp location mem cond_set = + match exp with + | Exp.UnOp (_, e, _) + | Exp.Exn e + | Exp.Lfield (e, _, _) + | Exp.Cast (_, e) + | Exp.Sizeof {dynamic_length= Some e} -> + check_expr_for_integer_overflow integer_type_widths e location mem cond_set + | Exp.BinOp (bop, lhs, rhs) -> + cond_set + |> check_binop_for_integer_overflow integer_type_widths bop ~lhs ~rhs location mem + |> check_expr_for_integer_overflow integer_type_widths lhs location mem + |> check_expr_for_integer_overflow integer_type_widths rhs location mem + | Exp.Lindex (e1, e2) -> + cond_set + |> check_expr_for_integer_overflow integer_type_widths e1 location mem + |> check_expr_for_integer_overflow integer_type_widths e2 location mem + | Exp.Closure {captured_vars} -> + List.fold captured_vars ~init:cond_set ~f:(fun cond_set (e, _, _) -> + check_expr_for_integer_overflow integer_type_widths e location mem cond_set ) + | Exp.Var _ | Exp.Const _ | Exp.Lvar _ | Exp.Sizeof {dynamic_length= None} -> + cond_set + + +let instantiate_cond : + Tenv.t + -> Typ.IntegerWidths.t + -> Procdesc.t + -> (Exp.t * Typ.t) list + -> Dom.Mem.t + -> BufferOverrunAnalysis.Payload.t + -> Location.t + -> PO.ConditionSet.checked_t = + fun tenv integer_type_widths callee_pdesc params caller_mem summary location -> + let callee_exit_mem = BufferOverrunSummary.get_output summary in + let callee_cond = BufferOverrunSummary.get_cond_set summary in + let rel_subst_map = + Sem.get_subst_map tenv integer_type_widths callee_pdesc params caller_mem callee_exit_mem in - (* Use a weak Hashtbl to prevent memory leaks (GC unnecessarily keeps invariant maps around) *) - let module WeakInvMapHashTbl = Caml.Weak.Make (struct - type t = Typ.Procname.t * invariant_map option - - let equal (pname1, _) (pname2, _) = Typ.Procname.equal pname1 pname2 - - let hash (pname, _) = Hashtbl.hash pname - end) in - let inv_map_cache = WeakInvMapHashTbl.create 100 in - fun pdesc tenv integer_type_widths -> - let pname = Procdesc.get_proc_name pdesc in - match WeakInvMapHashTbl.find_opt inv_map_cache (pname, None) with - | Some (_, Some inv_map) -> - inv_map - | Some (_, None) -> - (* this should never happen *) - assert false - | None -> - let inv_map = compute_invariant_map pdesc tenv integer_type_widths in - WeakInvMapHashTbl.add inv_map_cache (pname, Some inv_map) ; - inv_map - - -let memory_summary : local_decls -> CFG.t -> invariant_map -> memory_summary = - fun locals cfg inv_map -> - let exit_node_id = CFG.exit_node cfg |> CFG.Node.id in - match extract_post exit_node_id inv_map with - | Some exit_mem -> - exit_mem |> Dom.Mem.forget_locs locals |> Dom.Mem.unset_oenv - | None -> - Bottom - + 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 integer_type_widths callee_pdesc params caller_mem in + PO.ConditionSet.subst callee_cond eval_sym_trace rel_subst_map caller_rel pname location + + +let check_instr : + Procdesc.t + -> Tenv.t + -> Typ.IntegerWidths.t + -> CFG.Node.t + -> Sil.instr + -> Dom.Mem.t + -> PO.ConditionSet.checked_t + -> PO.ConditionSet.checked_t = + fun pdesc tenv integer_type_widths node instr mem cond_set -> + match instr with + | Sil.Load (_, exp, _, location) -> + cond_set + |> check_expr_for_array_access integer_type_widths exp location mem + |> check_expr_for_integer_overflow integer_type_widths exp location mem + | Sil.Store (lexp, _, rexp, location) -> + cond_set + |> check_expr_for_array_access integer_type_widths lexp location mem + |> check_expr_for_integer_overflow integer_type_widths lexp location mem + |> check_expr_for_integer_overflow integer_type_widths rexp location mem + | Sil.Call (_, Const (Cfun callee_pname), params, location, _) -> ( + let cond_set = + List.fold params ~init:cond_set ~f:(fun cond_set (exp, _) -> + check_expr_for_integer_overflow integer_type_widths exp location mem cond_set ) + in + match Models.Call.dispatch tenv callee_pname params with + | Some {Models.check} -> + let model_env = + let node_hash = CFG.Node.hash node in + let pname = Procdesc.get_proc_name pdesc in + BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths + in + check model_env mem cond_set + | None -> ( + match + Ondemand.analyze_proc_name ~caller_pdesc:pdesc callee_pname + |> Option.bind ~f:(fun callee_summary -> + BufferOverrunAnalysis.Payload.of_summary callee_summary + |> Option.map ~f:(fun payload -> (payload, Summary.get_proc_desc callee_summary)) + ) + with + | Some (callee_payload, callee_pdesc) -> + instantiate_cond tenv integer_type_widths callee_pdesc params mem callee_payload + location + |> PO.ConditionSet.join cond_set + | None -> + (* unknown call / no inferbo payload *) cond_set ) ) + | Sil.Prune (exp, location, _, _) -> + check_expr_for_integer_overflow integer_type_widths exp location mem cond_set + | _ -> + cond_set + + +let print_debug_info : Sil.instr -> Dom.Mem.t -> PO.ConditionSet.checked_t -> unit = + fun instr pre cond_set -> + L.(debug BufferOverrun Verbose) "@\n@\n================================@\n" ; + L.(debug BufferOverrun Verbose) "@[Pre-state : @,%a" Dom.Mem.pp pre ; + L.(debug BufferOverrun Verbose) "@]@\n@\n%a" (Sil.pp_instr ~print_types:true Pp.text) instr ; + L.(debug BufferOverrun Verbose) "@\n@\n@[%a" PO.ConditionSet.pp cond_set ; + L.(debug BufferOverrun Verbose) "@]@\n" ; + L.(debug BufferOverrun Verbose) "================================@\n@." + + +let check_instrs : + Procdesc.t + -> Tenv.t + -> Typ.IntegerWidths.t + -> CFG.t + -> CFG.Node.t + -> Instrs.not_reversed_t + -> Dom.Mem.t AbstractInterpreter.State.t + -> Checks.t + -> Checks.t = + fun pdesc tenv integer_type_widths cfg node instrs state checks -> + match state with + | _ when Instrs.is_empty instrs -> + checks + | {AbstractInterpreter.State.pre= Bottom} -> + checks + | {AbstractInterpreter.State.pre= NonBottom _ as pre; post} -> + if Instrs.nth_exists instrs 1 then + L.(die InternalError) "Did not expect several instructions" ; + let instr = Instrs.nth_exn instrs 0 in + let checks = + match post with + | Bottom -> + add_unreachable_code cfg node instr Instrs.empty checks + | NonBottom _ -> + checks + in + let cond_set = check_instr pdesc tenv integer_type_widths node instr pre checks.cond_set in + print_debug_info instr pre cond_set ; + {checks with cond_set} + + +let check_node : + Procdesc.t + -> Tenv.t + -> Typ.IntegerWidths.t + -> CFG.t + -> BufferOverrunAnalysis.invariant_map + -> Checks.t + -> CFG.Node.t + -> Checks.t = + fun pdesc tenv integer_type_widths cfg inv_map checks node -> + match BufferOverrunAnalysis.extract_state (CFG.Node.id node) inv_map with + | Some state -> + let instrs = CFG.instrs node in + check_instrs pdesc tenv integer_type_widths cfg node instrs state checks + | _ -> + checks + + +type checks = Checks.t let compute_checks : - Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> CFG.t -> invariant_map -> checks = - Report.check_proc + Procdesc.t + -> Tenv.t + -> Typ.IntegerWidths.t + -> CFG.t + -> BufferOverrunAnalysis.invariant_map + -> checks = + fun pdesc tenv integer_type_widths cfg inv_map -> + CFG.fold_nodes cfg ~f:(check_node pdesc tenv integer_type_widths cfg inv_map) ~init:Checks.empty + + +type checks_summary = PO.ConditionSet.summary_t + +let report_errors : Tenv.t -> Summary.t -> checks -> unit = + fun tenv summary {cond_set; unused_branches; unreachable_statements} -> + UnusedBranches.report tenv summary unused_branches ; + UnreachableStatements.report summary unreachable_statements ; + let report cond trace issue_type = + let location = PO.ConditionTrace.get_report_location trace in + let description ~markup = PO.description ~markup cond trace in + let trace = + let description = description ~markup:false in + Trace.Issue.make_err_trace ~description (PO.ConditionTrace.get_val_traces trace) + |> Errlog.concat_traces + in + Reporting.log_error summary ~loc:location ~ltr:trace issue_type (description ~markup:true) + in + PO.ConditionSet.report_errors ~report cond_set -let checks_summary : local_decls -> checks -> checks_summary = - fun locals checks -> Report.for_summary ~forget_locs:locals checks +let checks_summary : BufferOverrunAnalysis.local_decls -> checks -> checks_summary = + fun locals + Checks.({ cond_set + ; unused_branches= _ (* intra-procedural *) + ; unreachable_statements= _ (* intra-procedural *) }) -> + PO.ConditionSet.for_summary ~forget_locs:locals cond_set let checker : Callbacks.proc_callback_args -> Summary.t = fun {proc_desc; tenv; integer_type_widths; summary} -> - let inv_map = cached_compute_invariant_map proc_desc tenv integer_type_widths in + let inv_map = + BufferOverrunAnalysis.cached_compute_invariant_map proc_desc tenv integer_type_widths + in let underlying_exit_node = Procdesc.get_exit_node proc_desc in let pp_name f = F.pp_print_string f "bufferoverrun check" in NodePrinter.start_session ~pp_name underlying_exit_node ; let summary = let cfg = CFG.from_pdesc proc_desc in let checks = compute_checks proc_desc tenv integer_type_widths cfg inv_map in - Report.report_errors tenv summary checks ; - let locals = get_local_decls proc_desc in + report_errors tenv summary checks ; + let locals = BufferOverrunAnalysis.get_local_decls proc_desc in let cond_set = checks_summary locals checks in - let exit_mem = memory_summary locals cfg inv_map in + let exit_mem = BufferOverrunAnalysis.compute_summary locals cfg inv_map in let payload = (exit_mem, cond_set) in - Payload.update_summary payload summary + BufferOverrunAnalysis.Payload.update_summary payload summary in NodePrinter.finish_session underlying_exit_node ; summary diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.mli b/infer/src/bufferoverrun/bufferOverrunChecker.mli index b62aee7ba..aaee7beee 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.mli +++ b/infer/src/bufferoverrun/bufferOverrunChecker.mli @@ -8,13 +8,3 @@ open! IStd val checker : Callbacks.proc_callback_t - -module CFG = ProcCfg.NormalOneInstrPerNode - -type invariant_map - -val cached_compute_invariant_map : Procdesc.t -> Tenv.t -> Typ.IntegerWidths.t -> invariant_map - -val extract_pre : CFG.Node.id -> invariant_map -> BufferOverrunDomain.Mem.t option - -val extract_post : CFG.Node.id -> invariant_map -> BufferOverrunDomain.Mem.t option diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index ec951457e..2147c2746 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -53,7 +53,7 @@ module TransferFunctionsNodesBasicCost = struct module Domain = NodesBasicCostDomain type extras = - { inferbo_invariant_map: BufferOverrunChecker.invariant_map + { inferbo_invariant_map: BufferOverrunAnalysis.invariant_map ; integer_type_widths: Typ.IntegerWidths.t } let cost_atomic_instruction = BasicCost.one @@ -101,7 +101,7 @@ module TransferFunctionsNodesBasicCost = struct let exec_instr costmap ({ProcData.extras= {inferbo_invariant_map; integer_type_widths}} as pdata) node instr = let inferbo_mem = - Option.value_exn (BufferOverrunChecker.extract_pre (CFG.Node.id node) inferbo_invariant_map) + Option.value_exn (BufferOverrunAnalysis.extract_pre (CFG.Node.id node) inferbo_invariant_map) in let costmap = exec_instr_cost integer_type_widths inferbo_mem costmap pdata node instr in costmap @@ -151,7 +151,7 @@ module BoundMap = struct | _ -> ( let exit_state_opt = let instr_node_id = InstrCFG.last_of_underlying_node node |> InstrCFG.Node.id in - BufferOverrunChecker.extract_post instr_node_id inferbo_invariant_map + BufferOverrunAnalysis.extract_post instr_node_id inferbo_invariant_map in match exit_state_opt with | Some entry_mem -> @@ -740,7 +740,7 @@ let check_and_report_top_and_bottom cost proc_desc summary = let checker {Callbacks.tenv; proc_desc; integer_type_widths; summary} : Summary.t = let inferbo_invariant_map = - BufferOverrunChecker.cached_compute_invariant_map proc_desc tenv integer_type_widths + BufferOverrunAnalysis.cached_compute_invariant_map proc_desc tenv integer_type_widths in let node_cfg = NodeCFG.from_pdesc proc_desc in let proc_data = ProcData.make_default proc_desc tenv in diff --git a/infer/src/checkers/hoisting.ml b/infer/src/checkers/hoisting.ml index a65700345..28149bbd1 100644 --- a/infer/src/checkers/hoisting.ml +++ b/infer/src/checkers/hoisting.ml @@ -94,7 +94,7 @@ let get_issue_to_report tenv Call.({pname; node; params}) integer_type_widths in let instr_node_id = InstrCFG.last_of_underlying_node node |> InstrCFG.Node.id in let inferbo_invariant_map = Lazy.force inferbo_invariant_map in let inferbo_mem = - Option.value_exn (BufferOverrunChecker.extract_pre instr_node_id inferbo_invariant_map) + Option.value_exn (BufferOverrunAnalysis.extract_pre instr_node_id inferbo_invariant_map) in (* get the cost of the function call *) Cost.instantiate_cost integer_type_widths ~inferbo_caller_mem:inferbo_mem @@ -119,7 +119,7 @@ let checker Callbacks.({tenv; summary; proc_desc; integer_type_widths}) : Summar ~initial:(ReachingDefs.init_reaching_defs_with_formals proc_desc) in let inferbo_invariant_map = - lazy (BufferOverrunChecker.cached_compute_invariant_map proc_desc tenv integer_type_widths) + lazy (BufferOverrunAnalysis.cached_compute_invariant_map proc_desc tenv integer_type_widths) in (* get dominators *) let idom = Dominators.get_idoms proc_desc in diff --git a/infer/src/checkers/purity.ml b/infer/src/checkers/purity.ml index 53167d45b..724771565 100644 --- a/infer/src/checkers/purity.ml +++ b/infer/src/checkers/purity.ml @@ -23,7 +23,7 @@ module Payload = SummaryPayload.Make (struct end) type purity_extras = - {inferbo_invariant_map: BufferOverrunChecker.invariant_map; formals: Var.t list} + {inferbo_invariant_map: BufferOverrunAnalysis.invariant_map; formals: Var.t list} module TransferFunctions = struct module CFG = ProcCfg.Normal @@ -139,7 +139,7 @@ module TransferFunctions = struct CFG.Node.underlying_node node |> InstrCFG.last_of_underlying_node |> InstrCFG.Node.id in let inferbo_mem = - Option.value_exn (BufferOverrunChecker.extract_post node_id inferbo_invariant_map) + Option.value_exn (BufferOverrunAnalysis.extract_post node_id inferbo_invariant_map) in match instr with | Assign (ae, _, _) when is_heap_access ae -> @@ -185,7 +185,7 @@ let should_report pdesc = let checker {Callbacks.tenv; summary; proc_desc; integer_type_widths} : Summary.t = let proc_name = Procdesc.get_proc_name proc_desc in let inferbo_invariant_map = - BufferOverrunChecker.cached_compute_invariant_map proc_desc tenv integer_type_widths + BufferOverrunAnalysis.cached_compute_invariant_map proc_desc tenv integer_type_widths in let formals = Procdesc.get_formals proc_desc