From ace0ea3d8b7ba078e89a6190197d9c8e99738de5 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Fri, 27 Apr 2018 06:54:09 -0700 Subject: [PATCH] [inferbo] Do not reexecute for checking Summary: Now that we have the abstract state at the instruction level, we don't need to reexecute instructions during the checking phase and can just query the invariant map. Depends on D7608526 Reviewed By: skcho Differential Revision: D7775889 fbshipit-source-id: be17e2d --- .../src/bufferoverrun/bufferOverrunChecker.ml | 106 +++++++++--------- 1 file changed, 54 insertions(+), 52 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 172295f35..782070a5c 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -316,8 +316,6 @@ module Analyzer = AbstractInterpreter.Make (CFG) (TransferFunctions) module Report = struct module PO = BufferOverrunProofObligations - type extras = ProcData.no_extras - module ExitStatement = struct let non_significant_instr = function | Sil.(Abstract _ | Nullify _ | Remove_temps _) -> @@ -349,32 +347,28 @@ module Report = struct false end - let check_unreachable_code summary tenv (cfg: CFG.t) (node: CFG.node) instr rem_instrs mem = - match mem with - | NonBottom _ -> + let check_unreachable_code summary tenv (cfg: CFG.t) (node: CFG.node) instr rem_instrs = + match instr with + | Sil.Prune (_, _, _, (Ik_land_lor | Ik_bexp)) -> () - | Bottom -> - match instr with - | Sil.Prune (_, _, _, (Ik_land_lor | Ik_bexp)) -> - () - | Sil.Prune (cond, location, true_branch, _) -> - let i = match cond with Exp.Const (Const.Cint i) -> i | _ -> IntLit.zero in - let desc = - Errdesc.explain_condition_always_true_false tenv i cond (CFG.underlying_node node) - location - in - let exn = Exceptions.Condition_always_true_false (desc, not true_branch, __POS__) in - Reporting.log_warning summary ~loc:location exn - (* 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 -> - () - | _ -> - let location = Sil.instr_get_loc instr in - let desc = Errdesc.explain_unreachable_code_after location in - let exn = Exceptions.Unreachable_code_after (desc, __POS__) in - Reporting.log_error summary ~loc:location exn + | Sil.Prune (cond, location, true_branch, _) -> + let i = match cond with Exp.Const (Const.Cint i) -> i | _ -> IntLit.zero in + let desc = + Errdesc.explain_condition_always_true_false tenv i cond (CFG.underlying_node node) + location + in + let exn = Exceptions.Condition_always_true_false (desc, not true_branch, __POS__) in + Reporting.log_warning summary ~loc:location exn + (* 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 -> + () + | _ -> + let location = Sil.instr_get_loc instr in + let desc = Errdesc.explain_unreachable_code_after location in + let exn = Exceptions.Unreachable_code_after (desc, __POS__) in + Reporting.log_error summary ~loc:location exn let check_binop_array_access @@ -447,9 +441,9 @@ module Report = struct let check_instr - : extras ProcData.t -> CFG.node -> Sil.instr -> Dom.Mem.astate -> PO.ConditionSet.t + : Procdesc.t -> Tenv.t -> CFG.node -> Sil.instr -> Dom.Mem.astate -> PO.ConditionSet.t -> PO.ConditionSet.t = - fun {pdesc; tenv} node instr mem cond_set -> + fun pdesc tenv node instr mem cond_set -> let pname = Procdesc.get_proc_name pdesc in match instr with | Sil.Load (_, exp, _, location) | Sil.Store (exp, _, _, location) -> @@ -481,38 +475,46 @@ module Report = struct L.(debug BufferOverrun Verbose) "================================@\n@." - let rec check_instrs - : Specs.summary -> extras ProcData.t -> CFG.t -> CFG.node -> Sil.instr list -> Dom.Mem.astate - -> PO.ConditionSet.t -> PO.ConditionSet.t = - fun summary ({tenv} as pdata) cfg node instrs mem cond_set -> - match (mem, instrs) with - | _, [] | Bottom, _ -> + let check_instrs + : Specs.summary -> Procdesc.t -> Tenv.t -> CFG.t -> CFG.node -> Sil.instr list + -> Dom.Mem.astate AbstractInterpreter.state -> PO.ConditionSet.t -> PO.ConditionSet.t = + fun summary pdesc tenv cfg node instrs state cond_set -> + match (state, instrs) with + | _, [] | {AbstractInterpreter.pre= Bottom}, _ :: _ -> cond_set - | NonBottom _, instr :: rem_instrs -> - let cond_set = check_instr pdata node instr mem cond_set in - let mem = Analyzer.TransferFunctions.exec_instr mem pdata node instr in - let () = check_unreachable_code summary tenv cfg node instr rem_instrs mem in - print_debug_info instr mem cond_set ; - check_instrs summary pdata cfg node rem_instrs mem cond_set + | {AbstractInterpreter.pre= NonBottom _ as pre; post}, [instr] -> + let () = + match post with + | Bottom -> + check_unreachable_code summary tenv cfg node instr [] + | NonBottom _ -> + () + in + let cond_set = check_instr pdesc tenv node instr pre cond_set in + print_debug_info instr pre cond_set ; + cond_set + | _, _ :: _ :: _ -> + L.(die InternalError) "Did not expect several instructions" let check_node - : Specs.summary -> extras ProcData.t -> CFG.t -> Analyzer.invariant_map -> PO.ConditionSet.t - -> CFG.node -> PO.ConditionSet.t = - fun summary pdata cfg inv_map cond_set node -> - match Analyzer.extract_pre (CFG.id node) inv_map with - | Some mem -> + : Specs.summary -> Procdesc.t -> Tenv.t -> CFG.t -> Analyzer.invariant_map + -> PO.ConditionSet.t -> CFG.node -> PO.ConditionSet.t = + fun summary pdesc tenv cfg inv_map cond_set node -> + match Analyzer.extract_state (CFG.id node) inv_map with + | Some state -> let instrs = CFG.instrs node in - check_instrs summary pdata cfg node instrs mem cond_set + check_instrs summary pdesc tenv cfg node instrs state cond_set | _ -> cond_set let check_proc - : Specs.summary -> extras ProcData.t -> CFG.t -> Analyzer.invariant_map -> PO.ConditionSet.t = - fun summary pdata cfg inv_map -> + : Specs.summary -> Procdesc.t -> Tenv.t -> CFG.t -> Analyzer.invariant_map + -> PO.ConditionSet.t = + fun summary pdesc tenv cfg inv_map -> CFG.nodes cfg - |> List.fold ~f:(check_node summary pdata cfg inv_map) ~init:PO.ConditionSet.empty + |> List.fold ~f:(check_node summary pdesc tenv cfg inv_map) ~init:PO.ConditionSet.empty let make_err_trace : Trace.t -> string -> Errlog.loc_trace = @@ -577,13 +579,13 @@ let extract_post inv_map node = let compute_post : Specs.summary -> Analyzer.TransferFunctions.extras ProcData.t -> Summary.payload option = - fun summary ({pdesc} as pdata) -> + fun summary ({pdesc; tenv} as pdata) -> let cfg = CFG.from_pdesc pdesc in let inv_map = Analyzer.exec_pdesc ~initial:Dom.Mem.init pdata in let entry_mem = extract_post inv_map (CFG.start_node cfg) in let exit_mem = extract_post inv_map (CFG.exit_node cfg) in let cond_set = - Report.check_proc summary pdata cfg inv_map |> Report.report_errors summary pdesc + Report.check_proc summary pdesc tenv cfg inv_map |> Report.report_errors summary pdesc in match (entry_mem, exit_mem) with | Some entry_mem, Some exit_mem ->