diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index 4798a852f..632082302 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -118,14 +118,10 @@ module LivenessAnalysis = AbstractInterpreter.Make (BackwardCfg) (Scheduler.ReversePostorder) - (Liveness.Domain) (Liveness.TransferFunctions) module VarDomain = AbstractDomain.FiniteSet(Var.Set) -(* (reaching non-nullified vars) * (vars to nullify) *) -module NullifyDomain = AbstractDomain.Pair (VarDomain) (VarDomain) - (** computes the non-nullified reaching definitions at the end of each node by building on the results of a liveness analysis to be precise, what we want to compute is: to_nullify := (live_before U non_nullifed_reaching_defs) - live_after @@ -135,43 +131,53 @@ module NullifyDomain = AbstractDomain.Pair (VarDomain) (VarDomain) each pvar in to_nullify afer we finish the analysis. Nullify instructions speed up the analysis by enabling it to GC state that will no longer be read. *) module NullifyTransferFunctions = struct - type astate = NullifyDomain.astate + (* (reaching non-nullified vars) * (vars to nullify) *) + module Domain = AbstractDomain.Pair (VarDomain) (VarDomain) + module CFG = ProcCfg.Exceptional type extras = LivenessAnalysis.inv_map - type node_id = BackwardCfg.id let postprocess ((reaching_defs, _) as astate) node_id { ProcData.extras; } = match LivenessAnalysis.extract_state node_id extras with (* note: because the analysis backward, post and pre are reversed *) - | Some { LivenessAnalysis.post = live_before; pre = live_after; } -> + | Some { AbstractInterpreter.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) | None -> astate - let exec_instr ((active_defs, to_nullify) as astate) _ = function - | Sil.Letderef (lhs_id, _, _, _) -> - VarDomain.add (Var.of_id lhs_id) active_defs, to_nullify - | Sil.Call (lhs_ids, _, _, _, _) -> - let active_defs' = - IList.fold_left - (fun acc id -> VarDomain.add (Var.of_id id) acc) - active_defs - lhs_ids in - active_defs', to_nullify - | Sil.Set (Sil.Lvar lhs_pvar, _, _, _) -> - VarDomain.add (Var.of_pvar lhs_pvar) active_defs, to_nullify - | Sil.Set _ | Prune _ | Declare_locals _ | Stackop _ | Remove_temps _ - | Abstract _ -> - astate - | Sil.Nullify _ -> - failwith "Should not add nullify instructions before running nullify analysis!" + let is_last_instr_in_node instr node = + let rec is_last_instr instr = function + | [] -> true + | last_instr :: [] -> Sil.instr_compare instr last_instr = 0 + | _ :: instrs -> is_last_instr instr instrs in + is_last_instr instr (CFG.instrs node) + + let exec_instr ((active_defs, to_nullify) as astate) extras node instr = + let astate' = match instr with + | Sil.Letderef (lhs_id, _, _, _) -> + VarDomain.add (Var.of_id lhs_id) active_defs, to_nullify + | Sil.Call (lhs_ids, _, _, _, _) -> + let active_defs' = + IList.fold_left + (fun acc id -> VarDomain.add (Var.of_id id) acc) + active_defs + lhs_ids in + active_defs', to_nullify + | Sil.Set (Sil.Lvar lhs_pvar, _, _, _) -> + VarDomain.add (Var.of_pvar lhs_pvar) active_defs, to_nullify + | Sil.Set _ | Prune _ | Declare_locals _ | Stackop _ | Remove_temps _ + | Abstract _ -> + astate + | Sil.Nullify _ -> + failwith "Should not add nullify instructions before running nullify analysis!" in + if is_last_instr_in_node instr node + then postprocess astate' (CFG.id node) extras + else astate' end module NullifyAnalysis = - AbstractInterpreter.Make - (ProcCfg.Exceptional) - (Scheduler.ReversePostorder) - (NullifyDomain) + AbstractInterpreter.MakeNoCFG + (Scheduler.ReversePostorder (ProcCfg.Exceptional)) (NullifyTransferFunctions) let add_nullify_instrs tenv _ pdesc = diff --git a/infer/src/checkers/abstractInterpreter.ml b/infer/src/checkers/abstractInterpreter.ml index 0be623b09..d2485e618 100644 --- a/infer/src/checkers/abstractInterpreter.ml +++ b/infer/src/checkers/abstractInterpreter.ml @@ -11,18 +11,26 @@ open! Utils module L = Logging -module Make - (CFG : ProcCfg.S) - (Sched : Scheduler.S) - (A : AbstractDomain.S) - (T : TransferFunctions.S with type astate = A.astate and type node_id = CFG.id) = struct +type 'a state = { pre: 'a; post: 'a; visit_count: int; } - module S = Sched (CFG) - module M = ProcCfg.NodeIdMap (CFG) +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 + + val exec_pdesc : TF.extras ProcData.t -> inv_map + val compute_post : TF.extras ProcData.t -> TF.Domain.astate option +end + +module MakeNoCFG + (Sched : Scheduler.S) (TF : TransferFunctions.S with module CFG = Sched.CFG) = struct + + module CFG = Sched.CFG + module M = ProcCfg.NodeIdMap (Sched.CFG) + module A = TF.Domain - type state = { pre: A.astate; post: A.astate; visit_count: int; } (* invariant map from node id -> abstract state representing postcondition for node id *) - type inv_map = state M.t + type inv_map = A.astate state M.t (** extract the state of node [n] from [inv_map] *) let extract_state node_id inv_map = @@ -52,12 +60,17 @@ module Make let exec_instrs astate_acc instr = if A.is_bottom astate_acc then astate_acc - else T.exec_instr astate_acc proc_data instr in - let astate_post_instrs = IList.fold_left exec_instrs astate_pre (CFG.instrs node) in - T.postprocess astate_post_instrs node_id proc_data in + else TF.exec_instr astate_acc proc_data node instr in + (* hack to ensure that the transfer functions see every node *) + let node_instrs = match CFG.instrs node with + | [] -> + (* TODO: get rid of Stackop and replace it with Skip *) + [Sil.Stackop (Push, Location.dummy)] + | instrs -> instrs in + IList.fold_left exec_instrs astate_pre node_instrs in L.out "Post for node %a is %a@." CFG.pp_id node_id A.pp astate_post; let inv_map' = M.add node_id { pre=astate_pre; post=astate_post; visit_count; } inv_map in - inv_map', S.schedule_succs work_queue node in + inv_map', Sched.schedule_succs work_queue node in if M.mem node_id inv_map then let old_state = M.find node_id inv_map in let widened_pre = @@ -90,7 +103,7 @@ module Make match IList.flatten_options all_posts with | post :: posts -> Some (IList.fold_left A.join post posts) | [] -> None in - match S.pop work_queue with + match Sched.pop work_queue with | Some (_, [], work_queue') -> exec_worklist cfg work_queue' inv_map proc_data | Some (node, _, work_queue') -> @@ -104,7 +117,8 @@ module Make (* compute and return an invariant map for [cfg] *) 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 (S.empty cfg) M.empty proc_data in + let inv_map', work_queue' = + exec_node start_node A.initial (Sched.empty cfg) M.empty proc_data in exec_worklist cfg work_queue' inv_map' proc_data (* compute and return an invariant map for [pdesc] *) @@ -145,3 +159,5 @@ module Make end end +module Make (C : ProcCfg.S) (S : Scheduler.Make) (T : TransferFunctions.Make) = + MakeNoCFG (S (C)) (T (C)) diff --git a/infer/src/checkers/addressTaken.ml b/infer/src/checkers/addressTaken.ml index 4c00dea44..ddafe3aad 100644 --- a/infer/src/checkers/addressTaken.ml +++ b/infer/src/checkers/addressTaken.ml @@ -17,12 +17,10 @@ module PvarSet = PrettyPrintable.MakePPSet(struct module Domain = AbstractDomain.FiniteSet(PvarSet) -module TransferFunctions = struct - type astate = Domain.astate +module TransferFunctions (CFG : ProcCfg.S) = struct + module CFG = CFG + module Domain = Domain type extras = ProcData.no_extras - type node_id = ProcCfg.DefaultNode.id - - let postprocess = TransferFunctions.no_postprocessing let rec add_address_taken_pvars exp astate = match exp with | Sil.Lvar pvar -> @@ -37,7 +35,7 @@ module TransferFunctions = struct | Var _ | Sizeof _ -> astate - let exec_instr astate _ = function + let exec_instr astate _ _ = function | Sil.Set (_, Tptr _, rhs_exp, _) -> add_address_taken_pvars rhs_exp astate | Sil.Call (_, _, actuals, _, _) -> @@ -48,9 +46,8 @@ module TransferFunctions = struct | Sil.Set _ | Letderef _ | Prune _ | Nullify _ | Abstract _ | Remove_temps _ | Stackop _ | Declare_locals _ -> astate - end module Analyzer = AbstractInterpreter.Make - (ProcCfg.Exceptional) (Scheduler.ReversePostorder) (Domain) (TransferFunctions) + (ProcCfg.Exceptional) (Scheduler.ReversePostorder) (TransferFunctions) diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index 1fbb2ceda..013547977 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -268,12 +268,10 @@ let report_call_stack end_of_stack lookup_next_calls report pname loc calls = loop fst_call_loc Procname.Set.empty (start_trace, "") (fst_callee_pname, fst_call_loc)) calls -module TransferFunctions = struct - type astate = Domain.astate +module TransferFunctions (CFG : ProcCfg.S) = struct + module CFG = CFG + module Domain = Domain type extras = ProcData.no_extras - type node_id = ProcCfg.DefaultNode.id - - let postprocess = TransferFunctions.no_postprocessing (* This is specific to the @NoAllocation and @PerformanceCritical checker and the "unlikely" method is used to guard branches that are expected to run sufficiently @@ -327,7 +325,7 @@ module TransferFunctions = struct with T *) Sil.AnnotMap.fold add_call_for_annot map astate - let exec_instr astate { ProcData.pdesc; tenv; } = function + let exec_instr astate { ProcData.pdesc; tenv; } _ = function | Sil.Call ([id], Const (Cfun callee_pname), _, _, _) when is_unlikely callee_pname -> Domain.add_tracking_var (Var.of_id id) astate @@ -365,7 +363,6 @@ module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (Scheduler.ReversePostorder) - (Domain) (TransferFunctions) module Interprocedural = struct diff --git a/infer/src/checkers/copyPropagation.ml b/infer/src/checkers/copyPropagation.ml index eb53f2ee7..a8b9c8f6b 100644 --- a/infer/src/checkers/copyPropagation.ml +++ b/infer/src/checkers/copyPropagation.ml @@ -79,14 +79,12 @@ module Domain = struct |> gen lhs_var rhs_var end -module TransferFunctions = struct - type astate = Domain.astate +module TransferFunctions (CFG : ProcCfg.S) = struct + module CFG = CFG + module Domain = Domain type extras = ProcData.no_extras - type node_id = Cfg.Node.id - let postprocess = TransferFunctions.no_postprocessing - - let exec_instr astate _ = function + let exec_instr astate _ _ = function | Sil.Letderef (lhs_id, Sil.Lvar rhs_pvar, _, _) when not (Pvar.is_global rhs_pvar) -> Domain.gen (Var.of_id lhs_id) (Var.of_pvar rhs_pvar) astate | Sil.Set (Sil.Lvar lhs_pvar, _, Sil.Var rhs_id, _) when not (Pvar.is_global lhs_pvar) -> @@ -123,7 +121,6 @@ module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (Scheduler.ReversePostorder) - (Domain) (TransferFunctions) let checker { Callbacks.proc_desc; tenv; } = diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml index 6ebc9b68e..43345d9ec 100644 --- a/infer/src/checkers/liveness.ml +++ b/infer/src/checkers/liveness.ml @@ -18,12 +18,10 @@ module Domain = AbstractDomain.FiniteSet(Var.Set) (* compilers 101-style backward transfer functions for liveness analysis. gen a variable when it is read, kill the variable when it is assigned *) -module TransferFunctions = struct - type astate = Domain.astate +module TransferFunctions (CFG : ProcCfg.S) = struct + module CFG = CFG + module Domain = Domain type extras = ProcData.no_extras - type node_id = Cfg.Node.id - - let postprocess = TransferFunctions.no_postprocessing (* add all of the vars read in [exp] to the live set *) let exp_add_live exp astate = @@ -32,7 +30,7 @@ module TransferFunctions = struct IList.fold_left (fun astate_acc id -> Domain.add (Var.of_id id) astate_acc) astate ids in IList.fold_left (fun astate_acc pvar -> Domain.add (Var.of_pvar pvar) astate_acc) astate' pvars - let exec_instr astate _ = function + let exec_instr astate _ _ = function | Sil.Letderef (lhs_id, rhs_exp, _, _) -> Domain.remove (Var.of_id lhs_id) astate |> exp_add_live rhs_exp @@ -62,7 +60,6 @@ module Analyzer = AbstractInterpreter.Make (ProcCfg.Backward(ProcCfg.Exceptional)) (Scheduler.ReversePostorder) - (Domain) (TransferFunctions) let checker { Callbacks.proc_desc; tenv; } = diff --git a/infer/src/checkers/scheduler.ml b/infer/src/checkers/scheduler.ml index dbbf58bb4..0a890d9f3 100644 --- a/infer/src/checkers/scheduler.ml +++ b/infer/src/checkers/scheduler.ml @@ -12,7 +12,8 @@ open! Utils module F = Format module L = Logging -module type S = functor (CFG : ProcCfg.S) -> sig +module type S = sig + module CFG : ProcCfg.S type t (* schedule the successors of [node] *) @@ -21,12 +22,16 @@ module type S = functor (CFG : ProcCfg.S) -> sig predecessors, and the new schedule *) val pop : t -> (CFG.node * CFG.id list * t) option val empty : CFG.t -> t +end +module type Make = functor (CFG : ProcCfg.S) -> sig + include (S with module CFG = CFG) end (* simple scheduler that visits CFG nodes in reverse postorder. fast/precise for straightline code and conditionals; not as good for loops (may visit nodes after a loop multiple times). *) -module ReversePostorder : S = functor (CFG : ProcCfg.S) -> struct +module ReversePostorder (CFG : ProcCfg.S) = struct + module CFG = CFG module M = ProcCfg.NodeIdMap (CFG) module WorkUnit = struct diff --git a/infer/src/checkers/transferFunctions.ml b/infer/src/checkers/transferFunctions.ml index f8e5e09f1..4cc0afb82 100644 --- a/infer/src/checkers/transferFunctions.ml +++ b/infer/src/checkers/transferFunctions.ml @@ -9,17 +9,18 @@ open! Utils +(** Transfer functions that push abstract states across instructions. A typical client should + implement the Make signature to allow the transfer functions to be used with any kind of CFG. *) + module type S = sig - type astate (* abstract state to propagate *) + module CFG : ProcCfg.S + module Domain : AbstractDomain.S (* abstract domain whose state we propagate *) type extras (* read-only extra state (results of previous analyses, globals, etc.) *) - type node_id - - (* {A} instr {A'}. [caller_pdesc] is the procdesc of the current procedure *) - val exec_instr : astate -> extras ProcData.t -> Sil.instr -> astate - (* optional postprocessing step to be performed after executing node [id]. *) - val postprocess : astate -> node_id -> extras ProcData.t -> astate + (* {A} instr {A'}. [node] is the node of the current instruction *) + val exec_instr : Domain.astate -> extras ProcData.t -> CFG.node -> Sil.instr -> Domain.astate end -(* default postprocessing: do nothing *) -let no_postprocessing astate _ _ = astate +module type Make = functor (C : ProcCfg.S) -> sig + include (S with module CFG = C) +end diff --git a/infer/src/checkers/transferFunctions.mli b/infer/src/checkers/transferFunctions.mli new file mode 100644 index 000000000..3b75ea52a --- /dev/null +++ b/infer/src/checkers/transferFunctions.mli @@ -0,0 +1,24 @@ +(* + * 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. + *) + +(** Transfer functions that push abstract states across instructions. A typical client should + implement the Make signature to allow the transfer functions to be used with any kind of CFG. *) + +module type S = sig + module CFG : ProcCfg.S + module Domain : AbstractDomain.S (* abstract domain whose state we propagate *) + type extras (* read-only extra state (results of previous analyses, globals, etc.) *) + + (* {A} instr {A'}. [node] is the node of the current instruction *) + val exec_instr : Domain.astate -> extras ProcData.t -> CFG.node -> Sil.instr -> Domain.astate +end + +module type Make = functor (C : ProcCfg.S) -> sig + include (S with module CFG = C) +end diff --git a/infer/src/unit/abstractInterpreterTests.ml b/infer/src/unit/abstractInterpreterTests.ml index a73daf675..73953307c 100644 --- a/infer/src/unit/abstractInterpreterTests.ml +++ b/infer/src/unit/abstractInterpreterTests.ml @@ -48,28 +48,24 @@ module PathCountDomain = struct end -module PathCountTransferFunctions = struct - type astate = PathCountDomain.astate +module PathCountTransferFunctions (CFG : ProcCfg.S) = struct + module CFG = CFG + module Domain = PathCountDomain type extras = ProcData.no_extras - type node_id = Cfg.Node.id - - let postprocess = TransferFunctions.no_postprocessing (* just propagate the current path count *) - let exec_instr astate _ _ = astate + let exec_instr astate _ _ _ = astate end module NormalTestInterpreter = AnalyzerTester.Make (ProcCfg.Normal) (Scheduler.ReversePostorder) - (PathCountDomain) (PathCountTransferFunctions) module ExceptionalTestInterpreter = AnalyzerTester.Make (ProcCfg.Exceptional) (Scheduler.ReversePostorder) - (PathCountDomain) (PathCountTransferFunctions) let tests = @@ -186,7 +182,7 @@ let tests = ); invariant "1" ]; - ] |> NormalTestInterpreter.create_tests in + ] |> NormalTestInterpreter.create_tests ProcData.empty_extras in let exceptional_test_list = [ "try1", [ @@ -222,5 +218,5 @@ let tests = ); invariant "3" ]; - ] |> ExceptionalTestInterpreter.create_tests in + ] |> ExceptionalTestInterpreter.create_tests ProcData.empty_extras in "analyzer_tests_suite">:::(normal_test_list @ exceptional_test_list) diff --git a/infer/src/unit/addressTakenTests.ml b/infer/src/unit/addressTakenTests.ml index 2a7e91210..71130b5d5 100644 --- a/infer/src/unit/addressTakenTests.ml +++ b/infer/src/unit/addressTakenTests.ml @@ -14,7 +14,6 @@ module F = Format module TestInterpreter = AnalyzerTester.Make (ProcCfg.Exceptional) (Scheduler.ReversePostorder) - (AddressTaken.Domain) (AddressTaken.TransferFunctions) let tests = @@ -99,5 +98,5 @@ let tests = var_assign_var ~rhs_typ:int_ptr_typ "e" "f"; invariant "{ &b, &d, &f }" ]; - ] |> TestInterpreter.create_tests in + ] |> TestInterpreter.create_tests ProcData.empty_extras in "address_taken_suite">:::test_list diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index cbae176aa..baa146c43 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -139,16 +139,13 @@ end module Make (CFG : ProcCfg.S with type node = Cfg.Node.t) - (S : Scheduler.S) - (A : AbstractDomain.S) - (T : TransferFunctions.S - with type astate = A.astate and type extras = ProcData.no_extras - and type node_id = CFG.id) = struct + (S : Scheduler.Make) + (T : TransferFunctions.Make) = struct open StructuredSil - module I = AbstractInterpreter.Make (CFG) (S) (A) (T) - module M = ProcCfg.NodeIdMap (CFG) + module I = AbstractInterpreter.Make (CFG) (S) (T) + module M = I.M type assert_map = string M.t @@ -229,15 +226,15 @@ module Make Cfg.Procdesc.set_exit_node pdesc exit_node; pdesc, assert_map - let create_test test_program _ = + let create_test test_program extras _ = let pdesc, assert_map = structured_program_to_cfg test_program in - let inv_map = I.exec_pdesc (ProcData.make_default pdesc (Tenv.create ())) in + let inv_map = I.exec_pdesc (ProcData.make pdesc (Tenv.create ()) extras) 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 - pp_to_string A.pp state.post + pp_to_string I.A.pp state.post with Not_found -> "_|_" in if inv_str <> post_str then let error_msg = @@ -262,8 +259,8 @@ module Make |> F.flush_str_formatter in OUnit2.assert_failure assert_fail_message - let create_tests tests = + let create_tests extras tests = let open OUnit2 in - IList.map (fun (name, test_program) -> name>::create_test test_program) tests + IList.map (fun (name, test_program) -> name>::create_test test_program extras) tests end diff --git a/infer/src/unit/copyPropagationTests.ml b/infer/src/unit/copyPropagationTests.ml index b9e992d55..db7830191 100644 --- a/infer/src/unit/copyPropagationTests.ml +++ b/infer/src/unit/copyPropagationTests.ml @@ -14,7 +14,6 @@ module F = Format module TestInterpreter = AnalyzerTester.Make (ProcCfg.Exceptional) (Scheduler.ReversePostorder) - (CopyPropagation.Domain) (CopyPropagation.TransferFunctions) let tests = @@ -192,5 +191,5 @@ let tests = var_assign_var "c" "b"; invariant "{ &b -> &a, &c -> &b }" ]; - ] |> TestInterpreter.create_tests in + ] |> TestInterpreter.create_tests ProcData.empty_extras in "copy_propagation_test_suite">:::test_list diff --git a/infer/src/unit/livenessTests.ml b/infer/src/unit/livenessTests.ml index fefaa7e07..55817835a 100644 --- a/infer/src/unit/livenessTests.ml +++ b/infer/src/unit/livenessTests.ml @@ -14,7 +14,6 @@ module F = Format module TestInterpreter = AnalyzerTester.Make (ProcCfg.Backward(ProcCfg.Normal)) (Scheduler.ReversePostorder) - (Liveness.Domain) (Liveness.TransferFunctions) let tests = @@ -192,5 +191,5 @@ let tests = invariant "{ &b }"; var_assign_var "a" "b" ]; - ] |> TestInterpreter.create_tests in + ] |> TestInterpreter.create_tests ProcData.empty_extras in "liveness_test_suite">:::test_list