From c9b89b54dd87c38c0bd4c623f06b5a4e2c1f10c0 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Tue, 9 Oct 2018 07:51:50 -0700 Subject: [PATCH] Preparing for WeakTopologicalOrder-based abstract interpreter Reviewed By: ngorogiannis Differential Revision: D10069200 fbshipit-source-id: 5d6d5d12c --- infer/src/absint/AbstractInterpreter.ml | 235 +++++++++++------- infer/src/absint/AbstractInterpreter.mli | 27 +- infer/src/absint/LowerHil.ml | 2 +- infer/src/absint/LowerHil.mli | 2 +- infer/src/backend/preanal.ml | 8 +- .../src/bufferoverrun/bufferOverrunChecker.ml | 8 +- infer/src/checkers/BoundedCallTree.ml | 2 +- infer/src/checkers/NullabilityPreanalysis.ml | 2 +- infer/src/checkers/SimpleChecker.ml | 4 +- infer/src/checkers/Siof.ml | 2 +- infer/src/checkers/addressTaken.ml | 2 +- infer/src/checkers/annotationReachability.ml | 2 +- infer/src/checkers/control.ml | 6 +- infer/src/checkers/cost.ml | 6 +- infer/src/checkers/liveness.ml | 4 +- infer/src/checkers/reachingDefs.ml | 2 +- infer/src/unit/analyzerTester.ml | 25 +- infer/src/unit/inferunit.ml | 8 +- infer/src/unit/schedulerTests.ml | 32 +-- 19 files changed, 217 insertions(+), 162 deletions(-) diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 9b96916db..c2afd7f1d 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -17,14 +17,43 @@ type debug = When using LowerHil-AI, we're not interested in the underlying SIL instructions, it's the only case where want to disable it. *) -type 'a state = {pre: 'a; post: 'a; visit_count: int} +type exec_node_schedule_result = ReachedFixPoint | DidNotReachFixPoint + +module VisitCount : sig + type t = private int + + val first_time : t + + val succ : pdesc:Procdesc.t -> t -> t +end = struct + type t = int + + let first_time = 1 + + let succ ~pdesc visit_count = + let visit_count' = visit_count + 1 in + if visit_count' > Config.max_widens then + L.(die InternalError) + "Exceeded max widening threshold %d while analyzing %a. Please check your widening \ + operator or increase the threshold" + Config.max_widens Typ.Procname.pp (Procdesc.get_proc_name pdesc) ; + visit_count' +end + +module State = struct + type 'a t = {pre: 'a; post: 'a; visit_count: VisitCount.t} + + let pre {pre} = pre + + let post {post} = post +end module type S = sig module TransferFunctions : TransferFunctions.SIL module InvariantMap = TransferFunctions.CFG.Node.IdMap - type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t + type invariant_map = TransferFunctions.Domain.astate State.t InvariantMap.t val compute_post : ?debug:debug @@ -41,37 +70,30 @@ module type S = sig val exec_pdesc : TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> invariant_map - val extract_post : InvariantMap.key -> 'a state InvariantMap.t -> 'a option + val extract_post : InvariantMap.key -> 'a State.t InvariantMap.t -> 'a option - val extract_pre : InvariantMap.key -> 'a state InvariantMap.t -> 'a option + val extract_pre : InvariantMap.key -> 'a State.t InvariantMap.t -> 'a option val extract_state : InvariantMap.key -> 'a InvariantMap.t -> 'a option end -module MakeNoCFG - (Scheduler : Scheduler.S) - (TransferFunctions : TransferFunctions.SIL with module CFG = Scheduler.CFG) = -struct - module CFG = Scheduler.CFG +module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = struct + module CFG = TransferFunctions.CFG module Node = CFG.Node module TransferFunctions = TransferFunctions module InvariantMap = TransferFunctions.CFG.Node.IdMap module Domain = TransferFunctions.Domain - type invariant_map = Domain.astate state InvariantMap.t + type invariant_map = Domain.astate State.t InvariantMap.t (** extract the state of node [n] from [inv_map] *) let extract_state node_id inv_map = InvariantMap.find_opt node_id inv_map (** extract the postcondition of node [n] from [inv_map] *) - let extract_post node_id inv_map = - match extract_state node_id inv_map with Some state -> Some state.post | None -> None - + let extract_post node_id inv_map = extract_state node_id inv_map |> Option.map ~f:State.post (** extract the precondition of node [n] from [inv_map] *) - let extract_pre node_id inv_map = - match extract_state node_id inv_map with Some state -> Some state.pre | None -> None - + let extract_pre node_id inv_map = extract_state node_id inv_map |> Option.map ~f:State.pre let debug_absint_operation op node = let pp_name fmt = @@ -92,44 +114,49 @@ struct NodePrinter.finish_session underlying_node - let exec_node node astate_pre work_queue inv_map ({ProcData.pdesc} as proc_data) ~debug = - let node_id = Node.id node in - let update_inv_map pre ~visit_count = - let exec_instrs instrs = - if Config.write_html && debug <> DefaultNoExecInstr_UseFromLowerHilAbstractInterpreterOnly - then - NodePrinter.start_session - ~pp_name:(TransferFunctions.pp_session_name node) - (Node.underlying_node node) ; - let astate_post = - let compute_post pre instr = - try TransferFunctions.exec_instr pre proc_data node instr with exn -> - IExn.reraise_after exn ~f:(fun () -> - L.internal_error "In instruction %a@\n" (Sil.pp_instr Pp.text) instr ) - in - Instrs.fold ~f:compute_post ~init:pre instrs + let exec_instrs ~debug proc_data node node_id ~visit_count pre inv_map = + let on_instrs instrs = + if Config.write_html && debug <> DefaultNoExecInstr_UseFromLowerHilAbstractInterpreterOnly + then + NodePrinter.start_session + ~pp_name:(TransferFunctions.pp_session_name node) + (Node.underlying_node node) ; + let astate_post = + let compute_post pre instr = + try TransferFunctions.exec_instr pre proc_data node instr with exn -> + IExn.reraise_after exn ~f:(fun () -> + L.internal_error "In instruction %a@\n" (Sil.pp_instr Pp.text) instr ) in - if Config.write_html && debug <> DefaultNoExecInstr_UseFromLowerHilAbstractInterpreterOnly - then ( - L.d_strln - ( Format.asprintf "@[PRE: %a@]@\n@[INSTRS: %a@]@[POST: %a@]@." Domain.pp pre - (Instrs.pp Pp.text) instrs Domain.pp astate_post - |> Escape.escape_xml ) ; - NodePrinter.finish_session (Node.underlying_node node) ) ; - let inv_map' = InvariantMap.add node_id {pre; post= astate_post; visit_count} inv_map in - (inv_map', Scheduler.schedule_succs work_queue node) + Instrs.fold ~f:compute_post ~init:pre instrs in + if Config.write_html && debug <> DefaultNoExecInstr_UseFromLowerHilAbstractInterpreterOnly + then ( + L.d_strln + ( Format.asprintf "@[PRE: %a@]@\n@[INSTRS: %a@]@[POST: %a@]@." Domain.pp pre + (Instrs.pp Pp.text) instrs Domain.pp astate_post + |> Escape.escape_xml ) ; + NodePrinter.finish_session (Node.underlying_node node) ) ; + InvariantMap.add node_id {State.pre; post= astate_post; visit_count} inv_map + in + let instrs = CFG.instrs node in + if Instrs.is_empty instrs then (* hack to ensure that we call `exec_instr` on a node even if it has no instructions *) - let instrs = CFG.instrs node in - if Instrs.is_empty instrs then exec_instrs (Instrs.singleton Sil.skip_instr) - else exec_instrs instrs + on_instrs (Instrs.singleton Sil.skip_instr) + else on_instrs instrs + + + let exec_node ~debug ({ProcData.pdesc} as proc_data) node ~is_loop_head astate_pre inv_map = + let node_id = Node.id node in + let update_inv_map pre ~visit_count = + let inv_map' = exec_instrs ~debug proc_data node node_id ~visit_count pre inv_map in + (inv_map', DidNotReachFixPoint) in - if InvariantMap.mem node_id inv_map then ( + if InvariantMap.mem node_id inv_map then let old_state = InvariantMap.find node_id inv_map in let widened_pre = - if CFG.is_loop_head pdesc node then ( - let num_iters = old_state.visit_count in - let prev = old_state.pre in + if is_loop_head then ( + let num_iters = (old_state.State.visit_count :> int) in + let prev = old_state.State.pre in let next = astate_pre in let res = Domain.widen ~prev ~next ~num_iters in if Config.write_html then @@ -137,48 +164,69 @@ struct res ) else astate_pre in - if Domain.( <= ) ~lhs:widened_pre ~rhs:old_state.pre then (inv_map, work_queue) + if Domain.( <= ) ~lhs:widened_pre ~rhs:old_state.State.pre then (inv_map, ReachedFixPoint) else - let visit_count' = old_state.visit_count + 1 in - if visit_count' > Config.max_widens then - L.(die InternalError) - "Exceeded max widening threshold %d while analyzing %a. Please check your widening \ - operator or increase the threshold" - Config.max_widens Typ.Procname.pp (Procdesc.get_proc_name pdesc) ; - update_inv_map widened_pre ~visit_count:visit_count' ) - else (* first time visiting this node *) - update_inv_map astate_pre ~visit_count:1 - - - let rec exec_worklist cfg work_queue inv_map proc_data ~debug = - let compute_pre node inv_map = - let extract_post_ pred = extract_post (Node.id pred) inv_map in - CFG.fold_preds cfg node ~init:None ~f:(fun joined_post_opt pred -> - match extract_post_ pred with + let visit_count' = VisitCount.succ ~pdesc old_state.State.visit_count in + update_inv_map widened_pre ~visit_count:visit_count' + else + (* first time visiting this node *) + update_inv_map astate_pre ~visit_count:VisitCount.first_time + + + let compute_pre cfg node inv_map = + let extract_post_ pred = extract_post (Node.id pred) inv_map in + CFG.fold_preds cfg node ~init:None ~f:(fun joined_post_opt pred -> + match extract_post_ pred with + | None -> + joined_post_opt + | Some post as some_post -> ( + match joined_post_opt with | None -> - joined_post_opt - | Some post as some_post -> ( - match joined_post_opt with - | None -> - some_post - | Some joined_post -> - let res = Domain.join joined_post post in - if Config.write_html then - debug_absint_operation (`Join (joined_post, post, res)) node ; - Some res ) ) - in + some_post + | Some joined_post -> + let res = Domain.join joined_post post in + if Config.write_html then + debug_absint_operation (`Join (joined_post, post, res)) node ; + Some res ) ) + + + (** compute and return an invariant map for [pdesc] *) + let make_exec_pdesc ~exec_cfg_internal ({ProcData.pdesc} as proc_data) ~initial = + exec_cfg_internal ~debug:Default (CFG.from_pdesc pdesc) proc_data ~initial + + + (** compute and return the postcondition of [pdesc] *) + let make_compute_post ~exec_cfg_internal ?(debug = Default) ({ProcData.pdesc} as proc_data) + ~initial = + let cfg = CFG.from_pdesc pdesc in + let inv_map = exec_cfg_internal ~debug cfg proc_data ~initial in + extract_post (Node.id (CFG.exit_node cfg)) inv_map +end + +module MakeWithScheduler + (Scheduler : Scheduler.S) + (TransferFunctions : TransferFunctions.SIL with module CFG = Scheduler.CFG) = +struct + include AbstractInterpreterCommon (TransferFunctions) + + let rec exec_worklist ~debug cfg ({ProcData.pdesc} as proc_data) work_queue inv_map = match Scheduler.pop work_queue with | Some (_, [], work_queue') -> - exec_worklist cfg work_queue' inv_map proc_data ~debug + exec_worklist ~debug cfg proc_data work_queue' inv_map | Some (node, _, work_queue') -> let inv_map_post, work_queue_post = - match compute_pre node inv_map with - | Some astate_pre -> - exec_node node astate_pre work_queue' inv_map proc_data ~debug + match compute_pre cfg node inv_map with + | Some astate_pre -> ( + let is_loop_head = CFG.is_loop_head pdesc node in + match exec_node ~debug proc_data node ~is_loop_head astate_pre inv_map with + | inv_map, ReachedFixPoint -> + (inv_map, work_queue') + | inv_map, DidNotReachFixPoint -> + (inv_map, Scheduler.schedule_succs work_queue' node) ) | None -> (inv_map, work_queue') in - exec_worklist cfg work_queue_post inv_map_post proc_data ~debug + exec_worklist ~debug cfg proc_data work_queue_post inv_map_post | None -> inv_map @@ -186,25 +234,22 @@ struct (* compute and return an invariant map for [cfg] *) let exec_cfg_internal ~debug cfg proc_data ~initial = let start_node = CFG.start_node cfg in - let inv_map', work_queue' = - exec_node start_node initial (Scheduler.empty cfg) InvariantMap.empty proc_data ~debug + let inv_map, _did_not_reach_fix_point = + exec_node ~debug proc_data start_node ~is_loop_head:false initial InvariantMap.empty in - exec_worklist cfg work_queue' inv_map' proc_data ~debug + let work_queue = Scheduler.schedule_succs (Scheduler.empty cfg) start_node in + exec_worklist ~debug cfg proc_data work_queue inv_map let exec_cfg = exec_cfg_internal ~debug:Default - (* compute and return an invariant map for [pdesc] *) - let exec_pdesc ({ProcData.pdesc} as proc_data) = exec_cfg (CFG.from_pdesc pdesc) proc_data + let exec_pdesc = make_exec_pdesc ~exec_cfg_internal - (* compute and return the postcondition of [pdesc] *) - let compute_post ?(debug = Default) ({ProcData.pdesc} as proc_data) ~initial = - let cfg = CFG.from_pdesc pdesc in - let inv_map = exec_cfg_internal cfg proc_data ~initial ~debug in - extract_post (Node.id (CFG.exit_node cfg)) inv_map + let compute_post = make_compute_post ~exec_cfg_internal end -module MakeWithScheduler (C : ProcCfg.S) (S : Scheduler.Make) (T : TransferFunctions.MakeSIL) = - MakeNoCFG (S (C)) (T (C)) -module Make (C : ProcCfg.S) (T : TransferFunctions.MakeSIL) = - MakeWithScheduler (C) (Scheduler.ReversePostorder) (T) +module type Make = functor (TransferFunctions : TransferFunctions.SIL) -> S + with module TransferFunctions = TransferFunctions + +module MakeRPO (T : TransferFunctions.SIL) = + MakeWithScheduler (Scheduler.ReversePostorder (T.CFG)) (T) diff --git a/infer/src/absint/AbstractInterpreter.mli b/infer/src/absint/AbstractInterpreter.mli index 4915244ab..babf3c3db 100644 --- a/infer/src/absint/AbstractInterpreter.mli +++ b/infer/src/absint/AbstractInterpreter.mli @@ -9,7 +9,13 @@ open! IStd type debug = Default | DefaultNoExecInstr_UseFromLowerHilAbstractInterpreterOnly -type 'a state = {pre: 'a; post: 'a; visit_count: int} +module VisitCount : sig + type t +end + +module State : sig + type 'a t = {pre: 'a; post: 'a; visit_count: VisitCount.t} +end (** type of an intraprocedural abstract interpreter *) module type S = sig @@ -18,7 +24,7 @@ module type S = sig module InvariantMap = TransferFunctions.CFG.Node.IdMap (** invariant map from node id -> state representing postcondition for node id *) - type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t + type invariant_map = TransferFunctions.Domain.astate State.t InvariantMap.t val compute_post : ?debug:debug @@ -38,23 +44,18 @@ module type S = sig TransferFunctions.extras ProcData.t -> initial:TransferFunctions.Domain.astate -> invariant_map (** compute and return invariant map for the given procedure starting from [initial] *) - val extract_post : InvariantMap.key -> 'a state InvariantMap.t -> 'a option + val extract_post : InvariantMap.key -> 'a State.t InvariantMap.t -> 'a option (** extract the postcondition for a node id from the given invariant map *) - val extract_pre : InvariantMap.key -> 'a state InvariantMap.t -> 'a option + val extract_pre : InvariantMap.key -> 'a State.t InvariantMap.t -> 'a option (** extract the precondition for a node id from the given invariant map *) val extract_state : InvariantMap.key -> 'a InvariantMap.t -> 'a option (** extract the state for a node id from the given invariant map *) end -(** create an intraprocedural abstract interpreter from a scheduler and transfer functions *) -module MakeNoCFG - (Scheduler : Scheduler.S) - (TransferFunctions : TransferFunctions.SIL with module CFG = Scheduler.CFG) : - S with module TransferFunctions = TransferFunctions +module type Make = functor (TransferFunctions : TransferFunctions.SIL) -> S + with module TransferFunctions = TransferFunctions -(** create an intraprocedural abstract interpreter from a CFG and functors for creating a scheduler/ - transfer functions from a CFG *) -module Make (CFG : ProcCfg.S) (MakeTransferFunctions : TransferFunctions.MakeSIL) : - S with module TransferFunctions = MakeTransferFunctions(CFG) +(** create an intraprocedural abstract interpreter from transfer functions using the reverse post-order scheduler *) +module MakeRPO : Make diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml index aa36f0071..b2c87820d 100644 --- a/infer/src/absint/LowerHil.ml +++ b/infer/src/absint/LowerHil.ml @@ -90,7 +90,7 @@ module MakeAbstractInterpreterWithConfig (CFG : ProcCfg.S) (MakeTransferFunctions : TransferFunctions.MakeHIL) = struct - module Interpreter = AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (HilConfig)) + module Interpreter = AbstractInterpreter.MakeRPO (Make (MakeTransferFunctions) (HilConfig) (CFG)) let debug = AbstractInterpreter.DefaultNoExecInstr_UseFromLowerHilAbstractInterpreterOnly diff --git a/infer/src/absint/LowerHil.mli b/infer/src/absint/LowerHil.mli index ad839074f..8ac331123 100644 --- a/infer/src/absint/LowerHil.mli +++ b/infer/src/absint/LowerHil.mli @@ -39,7 +39,7 @@ module MakeAbstractInterpreterWithConfig (CFG : ProcCfg.S) (MakeTransferFunctions : TransferFunctions.MakeHIL) : sig module Interpreter : - module type of AbstractInterpreter.Make (CFG) (Make (MakeTransferFunctions) (HilConfig)) + module type of AbstractInterpreter.MakeRPO (Make (MakeTransferFunctions) (HilConfig) (CFG)) val compute_post : Interpreter.TransferFunctions.extras ProcData.t diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index a06ad1142..45b28fbbf 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -35,7 +35,7 @@ let add_abstraction_instructions pdesc = module BackwardCfg = ProcCfg.Backward (ProcCfg.Exceptional) -module LivenessAnalysis = AbstractInterpreter.Make (BackwardCfg) (Liveness.TransferFunctions) +module LivenessAnalysis = AbstractInterpreter.MakeRPO (Liveness.TransferFunctions (BackwardCfg)) module VarDomain = Liveness.Domain (** computes the non-nullified reaching definitions at the end of each node by building on the @@ -57,7 +57,7 @@ module NullifyTransferFunctions = struct let node_id = Procdesc.Node.get_id (CFG.Node.underlying_node node) in match LivenessAnalysis.extract_state node_id extras with (* note: because the analysis is backward, post and pre are reversed *) - | Some {AbstractInterpreter.post= live_before; pre= live_after} -> + | Some {AbstractInterpreter.State.post= live_before; pre= live_after} -> let to_nullify = VarDomain.diff (VarDomain.union live_before reaching_defs) live_after in let reaching_defs' = VarDomain.diff reaching_defs to_nullify in (reaching_defs', to_nullify) @@ -105,9 +105,7 @@ module NullifyTransferFunctions = struct let pp_session_name _node fmt = Format.pp_print_string fmt "nullify" end -module NullifyAnalysis = - AbstractInterpreter.MakeNoCFG - (Scheduler.ReversePostorder (ProcCfg.Exceptional)) (NullifyTransferFunctions) +module NullifyAnalysis = AbstractInterpreter.MakeRPO (NullifyTransferFunctions) let add_nullify_instrs pdesc tenv liveness_inv_map = let address_taken_vars = diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index dff34d994..55f206298 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -239,7 +239,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct end module CFG = ProcCfg.NormalOneInstrPerNode -module Analyzer = AbstractInterpreter.Make (CFG) (TransferFunctions) +module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (CFG)) type invariant_map = Analyzer.invariant_map @@ -572,16 +572,16 @@ module Report = struct -> CFG.t -> CFG.Node.t -> Instrs.not_reversed_t - -> Dom.Mem.astate AbstractInterpreter.state + -> Dom.Mem.astate AbstractInterpreter.State.t -> PO.ConditionSet.t -> PO.ConditionSet.t = fun summary pdesc tenv symbol_table cfg node instrs state cond_set -> match state with | _ when Instrs.is_empty instrs -> cond_set - | {AbstractInterpreter.pre= Bottom} -> + | {AbstractInterpreter.State.pre= Bottom} -> cond_set - | {AbstractInterpreter.pre= NonBottom _ as pre; post} -> + | {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 diff --git a/infer/src/checkers/BoundedCallTree.ml b/infer/src/checkers/BoundedCallTree.ml index 9830b39bd..c062b2f68 100644 --- a/infer/src/checkers/BoundedCallTree.ml +++ b/infer/src/checkers/BoundedCallTree.ml @@ -139,7 +139,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node fmt = F.pp_print_string fmt "crashcontext" end -module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (TransferFunctions) +module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (ProcCfg.Exceptional)) let loaded_stacktraces = (* Load all stacktraces defined in either Config.stacktrace or diff --git a/infer/src/checkers/NullabilityPreanalysis.ml b/infer/src/checkers/NullabilityPreanalysis.ml index 63b32d087..eb74bf92c 100644 --- a/infer/src/checkers/NullabilityPreanalysis.ml +++ b/infer/src/checkers/NullabilityPreanalysis.ml @@ -62,7 +62,7 @@ end (* Tracks when block variables of ObjC classes have been assigned to in constructors *) module FieldsAssignedInConstructorsChecker = - AbstractInterpreter.Make (ProcCfg.Normal) (TransferFunctions) + AbstractInterpreter.MakeRPO (TransferFunctions (ProcCfg.Normal)) let add_annot annot annot_name = ({Annot.class_name= annot_name; parameters= []}, true) :: annot diff --git a/infer/src/checkers/SimpleChecker.ml b/infer/src/checkers/SimpleChecker.ml index be24df249..893f6c605 100644 --- a/infer/src/checkers/SimpleChecker.ml +++ b/infer/src/checkers/SimpleChecker.ml @@ -78,13 +78,13 @@ module Make (Spec : Spec) : S = struct let pp_session_name _node fmt = F.pp_print_string fmt "simple checker" end - module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (TransferFunctions) + module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (ProcCfg.Exceptional)) let checker {Callbacks.proc_desc; tenv; summary} : Summary.t = let proc_name = Procdesc.get_proc_name proc_desc in let nodes = Procdesc.get_nodes proc_desc in let do_reporting node_id state = - let astate_set = state.AbstractInterpreter.post in + let astate_set = state.AbstractInterpreter.State.post in if not (Domain.is_empty astate_set) then (* should never fail since keys in the invariant map should always be real node id's *) let node = diff --git a/infer/src/checkers/Siof.ml b/infer/src/checkers/Siof.ml index 078d947f1..aef9c1a0d 100644 --- a/infer/src/checkers/Siof.ml +++ b/infer/src/checkers/Siof.ml @@ -209,7 +209,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node fmt = F.pp_print_string fmt "siof" end -module Analyzer = AbstractInterpreter.Make (ProcCfg.Normal) (TransferFunctions) +module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (ProcCfg.Normal)) let is_foreign current_tu v = match Pvar.get_translation_unit v with diff --git a/infer/src/checkers/addressTaken.ml b/infer/src/checkers/addressTaken.ml index 60b7337e4..ebef82b70 100644 --- a/infer/src/checkers/addressTaken.ml +++ b/infer/src/checkers/addressTaken.ml @@ -53,4 +53,4 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node fmt = Format.pp_print_string fmt "address taken" end -module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (TransferFunctions) +module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (ProcCfg.Exceptional)) diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index d59a1ca0b..fb572b09a 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -432,7 +432,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node fmt = F.pp_print_string fmt "annotation reachability" end -module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (TransferFunctions) +module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (ProcCfg.Exceptional)) let checker ({Callbacks.proc_desc; tenv; summary} as callback) : Summary.t = let initial = (AnnotReachabilityDomain.empty, NonBottom Domain.TrackingVar.empty) in diff --git a/infer/src/checkers/control.ml b/infer/src/checkers/control.ml index a84f209ad..1a81e7361 100644 --- a/infer/src/checkers/control.ml +++ b/infer/src/checkers/control.ml @@ -9,7 +9,7 @@ open! IStd module F = Format module L = Logging (* forward dependency analysis for computing set of variables that - affect the looping behavior of the program + affect the looping behavior of the program 1. perform a control flow dependency analysis by getting all the variables that appear in the guards of the loops. @@ -17,7 +17,7 @@ module L = Logging 2. for each control dependency per node, find its respective data dependency - 3. remove invariant vars in the loop from control vars + 3. remove invariant vars in the loop from control vars *) module VarSet = AbstractDomain.FiniteSet (Var) @@ -147,7 +147,7 @@ module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct F.fprintf fmt "control dependency analysis %a" CFG.Node.pp_id (CFG.Node.id node) end -module ControlDepAnalyzer = AbstractInterpreter.Make (CFG) (TransferFunctionsControlDeps) +module ControlDepAnalyzer = AbstractInterpreter.MakeRPO (TransferFunctionsControlDeps (CFG)) (* Filter CVs which are invariant in the loop where the CV originated from *) let remove_invariant_vars control_vars loop_inv_map = diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 8df95d147..3724d9e86 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -26,7 +26,6 @@ let expensive_threshold = BasicCost.of_int_exn 200 (* CFG modules used in several other modules *) module InstrCFG = ProcCfg.NormalOneInstrPerNode module NodeCFG = ProcCfg.Normal -module InstrCFGScheduler = Scheduler.ReversePostorder (InstrCFG) module Node = ProcCfg.DefaultNode (* Compute a map (node,instruction) -> basic_cost, where basic_cost is the @@ -99,8 +98,7 @@ module TransferFunctionsNodesBasicCost = struct let pp_session_name node fmt = F.fprintf fmt "cost(basic) %a" CFG.Node.pp_id (CFG.Node.id node) end -module AnalyzerNodesBasicCost = - AbstractInterpreter.MakeNoCFG (InstrCFGScheduler) (TransferFunctionsNodesBasicCost) +module AnalyzerNodesBasicCost = AbstractInterpreter.MakeRPO (TransferFunctionsNodesBasicCost) (* Map associating to each node a bound on the number of times it can be executed. This bound is computed using environments (map: val -> values), using the following @@ -720,7 +718,7 @@ module TransferFunctionsWCET = struct let pp_session_name _node fmt = F.pp_print_string fmt "cost(wcet)" end -module AnalyzerWCET = AbstractInterpreter.MakeNoCFG (InstrCFGScheduler) (TransferFunctionsWCET) +module AnalyzerWCET = AbstractInterpreter.MakeRPO (TransferFunctionsWCET) let check_and_report_top_and_bottom cost proc_desc summary = let report issue suffix = diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml index 08830ae1f..5e1da1091 100644 --- a/infer/src/checkers/liveness.ml +++ b/infer/src/checkers/liveness.ml @@ -75,7 +75,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct end module CFG = ProcCfg.OneInstrPerNode (ProcCfg.Backward (ProcCfg.Exceptional)) -module Analyzer = AbstractInterpreter.Make (CFG) (TransferFunctions) +module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (CFG)) (* It's fine to have a dead store on a type that uses the "scope guard" pattern. These types are only read in their destructors, and this is expected/ok. @@ -118,7 +118,7 @@ module CapturedByRefTransferFunctions (CFG : ProcCfg.S) = struct end module CapturedByRefAnalyzer = - AbstractInterpreter.Make (ProcCfg.Exceptional) (CapturedByRefTransferFunctions) + AbstractInterpreter.MakeRPO (CapturedByRefTransferFunctions (ProcCfg.Exceptional)) let get_captured_by_ref_invariant_map proc_desc proc_data = let cfg = ProcCfg.Exceptional.from_pdesc proc_desc in diff --git a/infer/src/checkers/reachingDefs.ml b/infer/src/checkers/reachingDefs.ml index e6f54638a..ac850ccee 100644 --- a/infer/src/checkers/reachingDefs.ml +++ b/infer/src/checkers/reachingDefs.ml @@ -64,4 +64,4 @@ let init_reaching_defs_with_formals pdesc = ReachingDefsMap.add (Var.of_pvar pvar) start_node_defs acc ) -module Analyzer = AbstractInterpreter.Make (ProcCfg.Normal) (TransferFunctionsReachingDefs) +module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctionsReachingDefs (ProcCfg.Normal)) diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 19fe1d0ef..834309b1a 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -147,10 +147,13 @@ module StructuredSil = struct make_call ?return args end -module Make (CFG : ProcCfg.S with type Node.t = Procdesc.Node.t) (T : TransferFunctions.MakeSIL) = +module MakeMake + (MakeAbstractInterpreter : AbstractInterpreter.Make) + (CFG : ProcCfg.S with type Node.t = Procdesc.Node.t) + (T : TransferFunctions.MakeSIL) = struct open StructuredSil - module I = AbstractInterpreter.Make (CFG) (T) + module I = MakeAbstractInterpreter (T (CFG)) module M = I.InvariantMap let structured_program_to_cfg program test_pname = @@ -239,15 +242,15 @@ struct (pdesc, assert_map) - let create_test test_program extras pp_opt ~initial test_pname _ = + let create_test test_program extras ~initial pp_opt test_pname _ = let pp_state = Option.value ~default:I.TransferFunctions.Domain.pp pp_opt in let pdesc, assert_map = structured_program_to_cfg test_program test_pname in let inv_map = I.exec_pdesc (ProcData.make pdesc (Tenv.create ()) extras) ~initial in let collect_invariant_mismatches node_id (inv_str, inv_label) error_msgs_acc = let post_str = try - let state = M.find node_id inv_map in - F.asprintf "%a" pp_state state.post + let {AbstractInterpreter.State.post} = M.find node_id inv_map in + F.asprintf "%a" pp_state post with Caml.Not_found -> "_|_" in if inv_str <> post_str then @@ -273,12 +276,20 @@ struct |> F.flush_str_formatter in OUnit2.assert_failure assert_fail_message +end + +module Make (CFG : ProcCfg.S with type Node.t = Procdesc.Node.t) (T : TransferFunctions.MakeSIL) = +struct + module AI_RPO = MakeMake (AbstractInterpreter.MakeRPO) (CFG) (T) + let ai_list = [("ai_rpo", AI_RPO.create_test)] let create_tests ?(test_pname = Typ.Procname.empty_block) ~initial ?pp_opt extras tests = let open OUnit2 in - List.map + List.concat_map ~f:(fun (name, test_program) -> - name >:: create_test test_program extras ~initial pp_opt test_pname ) + List.map ai_list ~f:(fun (ai_name, create_test) -> + name ^ "_" ^ ai_name >:: create_test test_program extras ~initial pp_opt test_pname ) + ) tests end diff --git a/infer/src/unit/inferunit.ml b/infer/src/unit/inferunit.ml index 585f221b6..35c25d445 100644 --- a/infer/src/unit/inferunit.ml +++ b/infer/src/unit/inferunit.ml @@ -31,19 +31,19 @@ let () = ; AccessTreeTests.tests ; AddressTakenTests.tests ; BoundedCallTreeTests.tests - ; DifferentialTests.tests ; DifferentialFiltersTests.tests + ; DifferentialTests.tests ; FileDiffTests.tests ; IListTests.tests ; JavaProfilerSamplesTest.tests + ; LivenessTests.tests ; PerfProfilerATDParserTest.tests ; ProcCfgTests.tests - ; LivenessTests.tests ; SchedulerTests.tests + ; SeverityTests.tests ; StacktraceTests.tests ; TaintTests.tests - ; TraceTests.tests - ; SeverityTests.tests ] + ; TraceTests.tests ] @ ClangTests.tests ) in let test_suite = "all" >::: tests in diff --git a/infer/src/unit/schedulerTests.ml b/infer/src/unit/schedulerTests.ml index cff5aae78..cbfc7663c 100644 --- a/infer/src/unit/schedulerTests.ml +++ b/infer/src/unit/schedulerTests.ml @@ -84,8 +84,7 @@ module MockProcCfg = struct let from_adjacency_list t = t - (* not called by the scheduler *) - let start_node _ = assert false + let start_node _ = 1 let exit_node _ = assert false @@ -117,21 +116,24 @@ let create_test test_graph expected_result _ = OUnit2.assert_equal ~pp_diff result expected_result +let inputs = + [ ("straightline", [(1, [2]); (2, [3]); (3, [4])], [1; 2; 3; 4]) + ; ("if_then_else", [(1, [2; 3]); (2, [4]); (3, [4]); (4, [5])], [1; 2; 3; 4; 5]) + ; ("if_then", [(1, [2; 4]); (2, [3]); (3, [4]); (4, [5])], [1; 2; 3; 4; 5]) + ; ( "diamond" + , [(1, [2; 3]); (2, [4]); (3, [4]); (4, [5; 6]); (5, [7]); (6, [7]); (7, [8])] + , [1; 2; 3; 4; 5; 6; 7; 8] ) + ; ( "switch" + , [(1, [2; 3; 4; 5]); (2, [6]); (3, [6]); (4, [6]); (5, [6]); (6, [7])] + , [1; 2; 3; 4; 5; 6; 7] ) + ; ( "nums_order_irrelevant" + , [(11, [10]); (1, [7; 2]); (2, [3; 11]); (7, [11]); (3, [7])] + , [1; 2; 3; 7; 11; 10] ) ] + + let tests = let open OUnit2 in let test_list = - [ ("straightline", [(1, [2]); (2, [3]); (3, [4])], [1; 2; 3; 4]) - ; ("if_then_else", [(1, [2; 3]); (2, [4]); (3, [4]); (4, [5])], [1; 2; 3; 4; 5]) - ; ("if_then", [(1, [2; 4]); (2, [3]); (3, [4]); (4, [5])], [1; 2; 3; 4; 5]) - ; ( "diamond" - , [(1, [2; 3]); (2, [4]); (3, [4]); (4, [5; 6]); (5, [7]); (6, [7]); (7, [8])] - , [1; 2; 3; 4; 5; 6; 7; 8] ) - ; ( "switch" - , [(1, [2; 3; 4; 5]); (2, [6]); (3, [6]); (4, [6]); (5, [6]); (6, [7])] - , [1; 2; 3; 4; 5; 6; 7] ) - ; ( "nums_order_irrelevant" - , [(11, [10]); (1, [7; 2]); (2, [3; 11]); (7, [11]); (3, [7])] - , [1; 2; 3; 7; 11; 10] ) ] - |> List.map ~f:(fun (name, test, expected) -> name >:: create_test test expected) + inputs |> List.map ~f:(fun (name, test, expected) -> name >:: create_test test expected) in "scheduler_suite" >::: test_list