diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 782070a5c..b988bb52e 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -313,6 +313,8 @@ end module CFG = ProcCfg.NormalOneInstrPerNode module Analyzer = AbstractInterpreter.Make (CFG) (TransferFunctions) +type invariant_map = Analyzer.invariant_map + module Report = struct module PO = BufferOverrunProofObligations @@ -572,18 +574,22 @@ module Report = struct PO.ConditionSet.check_all ~report cond_set end -let extract_post inv_map node = - let id = CFG.id node in - Analyzer.extract_post id inv_map +let extract_pre = Analyzer.extract_pre + +let extract_post = Analyzer.extract_post + +let compute_invariant_map : Procdesc.t -> Tenv.t -> invariant_map = + fun pdesc tenv -> + let pdata = ProcData.make_default pdesc tenv in + Analyzer.exec_pdesc ~initial:Dom.Mem.init pdata -let compute_post - : Specs.summary -> Analyzer.TransferFunctions.extras ProcData.t -> Summary.payload option = - fun summary ({pdesc; tenv} as pdata) -> +let compute_post : Specs.summary -> Procdesc.t -> Tenv.t -> Summary.payload option = + fun summary pdesc tenv -> + let inv_map = compute_invariant_map pdesc tenv in 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 entry_mem = extract_post (CFG.start_node cfg |> CFG.id) inv_map in + let exit_mem = extract_post (CFG.exit_node cfg |> CFG.id) inv_map in let cond_set = Report.check_proc summary pdesc tenv cfg inv_map |> Report.report_errors summary pdesc in @@ -603,8 +609,7 @@ let print_summary : Typ.Procname.t -> Dom.Summary.t -> unit = let checker : Callbacks.proc_callback_args -> Specs.summary = fun {proc_desc; tenv; summary} -> Preanal.do_preanalysis proc_desc tenv ; - let proc_data = ProcData.make_default proc_desc tenv in - match compute_post summary proc_data with + match compute_post summary proc_desc tenv with | Some post -> ( if Config.bo_debug >= 1 then let proc_name = Specs.get_proc_name summary in diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.mli b/infer/src/bufferoverrun/bufferOverrunChecker.mli index 634bceb76..18ac1900c 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.mli +++ b/infer/src/bufferoverrun/bufferOverrunChecker.mli @@ -11,9 +11,10 @@ open! IStd val checker : Callbacks.proc_callback_t -module TransferFunctions (C : ProcCfg.S) : sig - include TransferFunctions.SIL - with module CFG = C - and module Domain = BufferOverrunDomain.Mem - and type extras = ProcData.no_extras -end +module CFG = ProcCfg.NormalOneInstrPerNode + +type invariant_map + +val compute_invariant_map : Procdesc.t -> Tenv.t -> invariant_map + +val extract_pre : CFG.id -> invariant_map -> BufferOverrunDomain.Mem.t option diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 0ede0bd97..1190e4836 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -36,11 +36,7 @@ module Node = struct let equal_id = [%compare.equal : id] end -module NodesBasicCostDomain = struct - include AbstractDomain.Pair (BufferOverrunDomain.Mem) (CostDomain.NodeInstructionToCostMap) - - let init = (BufferOverrunDomain.Mem.init, CostDomain.NodeInstructionToCostMap.empty) -end +module NodesBasicCostDomain = CostDomain.NodeInstructionToCostMap (* Compute a map (node,instruction) -> basic_cost, where basic_cost is the cost known for a certain operation. For example for basic operation we @@ -49,10 +45,9 @@ end *) module TransferFunctionsNodesBasicCost = struct module CFG = InstrCFG - module InferboTransferFunctions = BufferOverrunChecker.TransferFunctions (CFG) module Domain = NodesBasicCostDomain - type extras = InferboTransferFunctions.extras + type extras = BufferOverrunChecker.invariant_map let cost_atomic_instruction = Itv.Bound.one @@ -78,10 +73,10 @@ module TransferFunctionsNodesBasicCost = struct astate' - let exec_instr (inferbo_mem, costmap) pdata node instr = - let inferbo_mem = InferboTransferFunctions.exec_instr inferbo_mem pdata node instr in + let exec_instr costmap ({ProcData.extras= inferbo_invariant_map} as pdata) node instr = + let inferbo_mem = BufferOverrunChecker.extract_pre (CFG.id node) inferbo_invariant_map in let costmap = exec_instr_cost inferbo_mem costmap pdata node instr in - (inferbo_mem, costmap) + costmap let pp_session_name node fmt = F.fprintf fmt "cost(basic) %a" CFG.pp_id (CFG.id node) @@ -141,7 +136,7 @@ module BoundMap = struct NonBottom env - let compute_upperbound_map node_cfg invariant_map_NodesBasicCost data_invariant_map + let compute_upperbound_map node_cfg inferbo_invariant_map data_invariant_map control_invariant_map = let fparam = Procdesc.get_formals node_cfg in let pname = Procdesc.get_proc_name node_cfg in @@ -154,10 +149,10 @@ module BoundMap = struct | _ -> let entry_state_opt = let instr_node_id = InstrCFG.of_underlying_node node |> InstrCFG.id in - AnalyzerNodesBasicCost.extract_pre instr_node_id invariant_map_NodesBasicCost + BufferOverrunChecker.extract_pre instr_node_id inferbo_invariant_map in match entry_state_opt with - | Some (entry_mem, _) -> + | Some entry_mem -> (* compute all the dependencies, i.e. set of variables that affect the control flow upto the node *) let all_deps = Control.compute_all_deps data_invariant_map control_invariant_map node @@ -543,7 +538,7 @@ module TransferFunctionsWCET = struct let cost_node = let instr_node_id = CFG.id node in match AnalyzerNodesBasicCost.extract_post instr_node_id invariant_map_cost with - | Some (_, node_map) -> + | Some node_map -> L.(debug Analysis Medium) "@\n AnalyzerWCET] Final map for node: %a @\n" CFG.pp_id instr_node_id ; map_cost trees node_map @@ -583,6 +578,7 @@ let check_and_report_infinity cost proc_desc summary = let checker {Callbacks.tenv; summary; proc_desc} : Specs.summary = Preanal.do_preanalysis proc_desc tenv ; + let inferbo_invariant_map = BufferOverrunChecker.compute_invariant_map proc_desc tenv in let proc_data = ProcData.make_default proc_desc tenv in let node_cfg = NodeCFG.from_pdesc proc_desc in (* computes the data dependencies: node -> (var -> var set) *) @@ -597,13 +593,14 @@ let checker {Callbacks.tenv; summary; proc_desc} : Specs.summary = in let instr_cfg = InstrCFG.from_pdesc proc_desc in let invariant_map_NodesBasicCost = + let proc_data = ProcData.make proc_desc tenv inferbo_invariant_map in (*compute_WCET cfg invariant_map min_trees in *) - AnalyzerNodesBasicCost.exec_cfg instr_cfg proc_data ~initial:NodesBasicCostDomain.init + AnalyzerNodesBasicCost.exec_cfg instr_cfg proc_data ~initial:NodesBasicCostDomain.empty ~debug:true in (* given the semantics computes the upper bound on the number of times a node could be executed *) let bound_map = - BoundMap.compute_upperbound_map node_cfg invariant_map_NodesBasicCost data_dep_invariant_map + BoundMap.compute_upperbound_map node_cfg inferbo_invariant_map data_dep_invariant_map control_dep_invariant_map in let constraints = StructuralConstraints.compute_structural_constraints node_cfg in