diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index a4015e268..06241e1df 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -113,7 +113,7 @@ module NullifyTransferFunctions = struct (* (reaching non-nullified vars) * (vars to nullify) *) module Domain = AbstractDomain.Pair (VarDomain) (VarDomain) module CFG = ProcCfg.Exceptional - type extras = LivenessAnalysis.inv_map + type extras = LivenessAnalysis.invariant_map let postprocess ((reaching_defs, _) as astate) node { ProcData.extras; } = let node_id = (CFG.underlying_id node), ProcCfg.Node_index in diff --git a/infer/src/checkers/AbstractInterpreter.mli b/infer/src/checkers/AbstractInterpreter.mli new file mode 100644 index 000000000..1ad598392 --- /dev/null +++ b/infer/src/checkers/AbstractInterpreter.mli @@ -0,0 +1,60 @@ +(* + * Copyright (c) 2016 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + *) + +type 'a state = { pre: 'a; post: 'a; visit_count: int; } + +(** type of an intraprocedural abstract interpreter *) +module type S = sig + module TransferFunctions : TransferFunctions.S + + module InvariantMap : Map.S with type key = TransferFunctions.CFG.id + + (** create an interprocedural abstract interpreter given logic for handling summaries *) + module Interprocedural + (Summary : Summary.S with type summary = TransferFunctions.Domain.astate) : + sig + val checker : Callbacks.proc_callback_args -> TransferFunctions.extras -> + TransferFunctions.Domain.astate option + end + + (** invariant map from node id -> state representing postcondition for node id *) + type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t + + (** compute and return the postcondition for the given procedure *) + val compute_post : TransferFunctions.extras ProcData.t -> TransferFunctions.Domain.astate option + + (** compute and return invariant map for the given CFG/procedure. *) + val exec_cfg : TransferFunctions.CFG.t -> TransferFunctions.extras ProcData.t -> invariant_map + + (** compute and return invariant map for the given procedure. *) + val exec_pdesc : TransferFunctions.extras ProcData.t -> invariant_map + + (** extract the postcondition for a node id from the given invariant map *) + val extract_post : InvariantMap.key -> 'a state InvariantMap.t -> 'a option + + (** extract the precondition for a node id from the given invariant map *) + val extract_pre : InvariantMap.key -> 'a state InvariantMap.t -> 'a option + + (** extract the state for a node id from the given invariant map *) + val extract_state : InvariantMap.key -> 'a InvariantMap.t -> 'a option +end + +(** create an intraprocedural abstract interpreter from a scheduler and transfer functions *) +module MakeNoCFG + (Scheduler : Scheduler.S) + (TransferFunctions : TransferFunctions.S with module CFG = Scheduler.CFG) : + 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) + (MakeScheduler : Scheduler.Make) + (MakeTransferFunctions : TransferFunctions.Make) : + S with module TransferFunctions = MakeTransferFunctions(CFG) diff --git a/infer/src/checkers/abstractInterpreter.ml b/infer/src/checkers/abstractInterpreter.ml index bee8c7b0a..e0d2b91a6 100644 --- a/infer/src/checkers/abstractInterpreter.ml +++ b/infer/src/checkers/abstractInterpreter.ml @@ -14,27 +14,39 @@ module L = Logging type 'a state = { pre: 'a; post: 'a; visit_count: int; } module type S = sig - module TF : TransferFunctions.S - module M : Map.S with type key = TF.CFG.id - type inv_map = TF.Domain.astate state M.t + module TransferFunctions : TransferFunctions.S + module InvariantMap : Map.S with type key = TransferFunctions.CFG.id + module Interprocedural + (Summary : Summary.S with type summary = TransferFunctions.Domain.astate) : + sig + val checker : Callbacks.proc_callback_args -> TransferFunctions.extras -> + TransferFunctions.Domain.astate option + end + + type invariant_map = TransferFunctions.Domain.astate state InvariantMap.t - val exec_pdesc : TF.extras ProcData.t -> inv_map - val compute_post : TF.extras ProcData.t -> TF.Domain.astate option + val compute_post : TransferFunctions.extras ProcData.t -> TransferFunctions.Domain.astate option + val exec_cfg : TransferFunctions.CFG.t -> TransferFunctions.extras ProcData.t -> invariant_map + val exec_pdesc : TransferFunctions.extras ProcData.t -> invariant_map + val extract_post : InvariantMap.key -> 'a state InvariantMap.t -> 'a option + val extract_pre : InvariantMap.key -> 'a state InvariantMap.t -> 'a option + val extract_state : InvariantMap.key -> 'a InvariantMap.t -> 'a option end module MakeNoCFG - (Sched : Scheduler.S) (TF : TransferFunctions.S with module CFG = Sched.CFG) = struct + (Scheduler : Scheduler.S) + (TransferFunctions : TransferFunctions.S with module CFG = Scheduler.CFG) = struct - module CFG = Sched.CFG - module M = ProcCfg.NodeIdMap (Sched.CFG) - module A = TF.Domain + module CFG = Scheduler.CFG + module InvariantMap = ProcCfg.NodeIdMap (CFG) + module TransferFunctions = TransferFunctions + module Domain = TransferFunctions.Domain - (* invariant map from node id -> abstract state representing postcondition for node id *) - type inv_map = A.astate state M.t + type invariant_map = Domain.astate state InvariantMap.t (** extract the state of node [n] from [inv_map] *) let extract_state node_id inv_map = - try Some (M.find node_id inv_map) + try Some (InvariantMap.find node_id inv_map) with Not_found -> None (** extract the postcondition of node [n] from [inv_map] *) @@ -53,23 +65,24 @@ module MakeNoCFG let node_id = CFG.id node in let update_inv_map pre visit_count = let compute_post (pre, inv_map) (instr, id_opt) = - let post = TF.exec_instr pre proc_data node instr in + let post = TransferFunctions.exec_instr pre proc_data node instr in match id_opt with - | Some id -> post, M.add id { pre; post; visit_count; } inv_map + | Some id -> post, InvariantMap.add id { pre; post; visit_count; } inv_map | None -> post, inv_map in (* hack to ensure that we call `exec_instr` on a node even if it has no instructions *) let instr_ids = match CFG.instr_ids node with | [] -> [Sil.skip_instr, None] | l -> l in let astate_post, inv_map_post = IList.fold_left compute_post (pre, inv_map) instr_ids in - let inv_map'' = M.add node_id { pre; post=astate_post; visit_count; } inv_map_post in - inv_map'', Sched.schedule_succs work_queue node in - if M.mem node_id inv_map + let inv_map'' = + InvariantMap.add node_id { pre; post=astate_post; visit_count; } inv_map_post in + inv_map'', Scheduler.schedule_succs work_queue node in + if InvariantMap.mem node_id inv_map then - let old_state = M.find node_id inv_map in + let old_state = InvariantMap.find node_id inv_map in let widened_pre = - A.widen ~prev:old_state.pre ~next:astate_pre ~num_iters:old_state.visit_count in - if A.(<=) ~lhs:widened_pre ~rhs:old_state.pre + Domain.widen ~prev:old_state.pre ~next:astate_pre ~num_iters:old_state.visit_count in + if Domain.(<=) ~lhs:widened_pre ~rhs:old_state.pre then inv_map, work_queue else update_inv_map widened_pre (old_state.visit_count + 1) else @@ -86,9 +99,9 @@ module MakeNoCFG let extract_pre_f acc pred = extract_pre (CFG.id pred) inv_map :: acc in let all_posts = IList.fold_left extract_pre_f normal_posts (CFG.exceptional_preds cfg node) in match IList.flatten_options all_posts with - | post :: posts -> Some (IList.fold_left A.join post posts) + | post :: posts -> Some (IList.fold_left Domain.join post posts) | [] -> None in - match Sched.pop work_queue with + match Scheduler.pop work_queue with | Some (_, [], work_queue') -> exec_worklist cfg work_queue' inv_map proc_data | Some (node, _, work_queue') -> @@ -103,7 +116,7 @@ module MakeNoCFG let exec_cfg cfg proc_data = let start_node = CFG.start_node cfg in let inv_map', work_queue' = - exec_node start_node A.initial (Sched.empty cfg) M.empty proc_data in + exec_node start_node Domain.initial (Scheduler.empty cfg) InvariantMap.empty proc_data in exec_worklist cfg work_queue' inv_map' proc_data (* compute and return an invariant map for [pdesc] *) @@ -116,7 +129,7 @@ module MakeNoCFG let inv_map = exec_cfg cfg proc_data in extract_post (CFG.id (CFG.exit_node cfg)) inv_map - module Interprocedural (Summ : Summary.S with type summary = A.astate) = struct + module Interprocedural (Summ : Summary.S with type summary = Domain.astate) = struct let checker { Callbacks.get_proc_desc; proc_desc; proc_name; tenv; } extras = let analyze_ondemand_ _ pdesc = diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index fbc8523be..862a54c05 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -163,7 +163,7 @@ module Make open StructuredSil module I = AbstractInterpreter.Make (CFG) (S) (T) - module M = I.M + module M = I.InvariantMap type assert_map = string M.t @@ -245,7 +245,7 @@ module Make pdesc, assert_map let create_test test_program extras pp_opt test_pname _ = - let pp_state = Option.default I.A.pp pp_opt in + let pp_state = Option.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) in