From fd219ae4577d2ae09cbf25a93ffc8e9afe60d4d9 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 13 Apr 2021 09:19:38 -0700 Subject: [PATCH] [absint] Give instr index to `exec_instr` to get inferbo result Summary: In order to use Inferbo's analysis result, a checker should know current instruction index. However, for the checkers using `ProcCfg.Normal` CFG, it was impossible to get the instruction index. To solve the issue, this diff changes the AbsInt framework to give the index together to `exec_instr`. Reviewed By: ezgicicek Differential Revision: D27680894 fbshipit-source-id: 1dc8ff0fb --- infer/src/IR/Instrs.ml | 26 ++++-- infer/src/IR/Instrs.mli | 4 +- infer/src/absint/AbstractInterpreter.ml | 12 +-- infer/src/absint/LowerHil.ml | 12 +-- infer/src/absint/LowerHil.mli | 8 +- infer/src/absint/ProcCfg.ml | 81 ++++++++++--------- infer/src/absint/ProcCfg.mli | 31 ++++--- infer/src/absint/TransferFunctions.ml | 3 +- infer/src/absint/TransferFunctions.mli | 7 +- .../backend/ClosureSubstSpecializedMethod.ml | 2 +- infer/src/backend/ClosuresSubstitution.ml | 2 +- infer/src/backend/Devirtualizer.ml | 2 +- infer/src/backend/preanal.ml | 2 +- .../bufferoverrun/bufferOverrunAnalysis.ml | 10 ++- .../checkers/ConfigChecksBetweenMarkers.ml | 2 +- infer/src/checkers/NullabilityPreanalysis.ml | 2 +- infer/src/checkers/PurityAnalysis.ml | 2 +- infer/src/checkers/RequiredProps.ml | 2 +- infer/src/checkers/SelfInBlock.ml | 2 +- infer/src/checkers/Siof.ml | 2 +- infer/src/checkers/addressTaken.ml | 2 +- infer/src/checkers/annotationReachability.ml | 2 +- infer/src/checkers/control.ml | 2 +- infer/src/checkers/functionPointers.ml | 2 +- infer/src/checkers/liveness.ml | 4 +- infer/src/checkers/reachingDefs.ml | 2 +- infer/src/checkers/uninit.ml | 2 +- infer/src/concurrency/RacerDProcAnalysis.ml | 2 +- infer/src/concurrency/starvation.ml | 2 +- infer/src/cost/ConfigImpactAnalysis.ml | 7 +- infer/src/cost/costInstantiate.ml | 17 ++-- infer/src/cost/costInstantiate.mli | 5 +- infer/src/cost/hoisting.ml | 10 ++- infer/src/dotnet/ResourceLeaksCS.ml | 2 +- .../labs/00_dummy_checker/ResourceLeaks.ml | 2 +- .../labs/01_integer_domain/ResourceLeaks.ml | 4 +- .../src/labs/02_domain_join/ResourceLeaks.ml | 4 +- infer/src/labs/03_domain_top/ResourceLeaks.ml | 4 +- .../labs/04_interprocedural/ResourceLeaks.ml | 2 +- .../ResourceLeaks.ml | 2 +- infer/src/labs/ResourceLeaks.ml | 2 +- infer/src/quandary/TaintAnalysis.ml | 2 +- infer/src/unit/abstractInterpreterTests.ml | 2 +- infer/src/unit/schedulerTests.ml | 2 + 44 files changed, 177 insertions(+), 124 deletions(-) diff --git a/infer/src/IR/Instrs.ml b/infer/src/IR/Instrs.ml index 2cfc3d672..ecce4228c 100644 --- a/infer/src/IR/Instrs.ml +++ b/infer/src/IR/Instrs.ml @@ -22,6 +22,8 @@ module RevArray : sig val last_opt : 'a t -> 'a option val fold : ('a t, 'a, 'accum) Container.fold + + val foldi : 'a t -> init:'accum -> f:(int -> 'accum -> 'a -> 'accum) -> 'accum end = struct type 'a t = 'a Array.t @@ -38,6 +40,13 @@ end = struct let fold a ~init ~f = let f = Fn.flip f in Array.fold_right a ~init ~f + + + let foldi a ~init ~f = + let idx = ref (Array.length a) in + Array.fold_right a ~init ~f:(fun elt acc -> + decr idx ; + f !idx acc elt ) end type reversed @@ -168,6 +177,18 @@ let fold (type r) (t : r t) ~init ~f = RevArray.fold rev_instrs ~init ~f +let foldi (type r) (t : r t) ~init ~f = + match t with + | Empty -> + init + | Singleton instr -> + f 0 init instr + | NotReversed instrs -> + Array.foldi instrs ~init ~f + | Reversed rev_instrs -> + RevArray.foldi rev_instrs ~init ~f + + let iter t ~f = Container.iter ~fold t ~f let exists t ~f = Container.exists ~iter t ~f @@ -228,8 +249,3 @@ let instrs_get_normal_vars instrs = |> Ident.hashqueue_of_sequence ~init:res ) in fold ~init:(Ident.HashQueue.create ()) ~f:do_instr instrs |> Ident.HashQueue.keys - - -let find_instr_index instrs instr = - let instrs = get_underlying_not_reversed instrs in - Array.findi instrs ~f:(fun _index i -> Sil.equal_instr i instr) |> Option.map ~f:fst diff --git a/infer/src/IR/Instrs.mli b/infer/src/IR/Instrs.mli index bf19728ee..48a0afe1c 100644 --- a/infer/src/IR/Instrs.mli +++ b/infer/src/IR/Instrs.mli @@ -65,12 +65,12 @@ val last : _ t -> Sil.instr option val find_map : _ t -> f:(Sil.instr -> 'a option) -> 'a option -val find_instr_index : not_reversed t -> Sil.instr -> int option - val pp : Pp.env -> Format.formatter -> _ t -> unit val fold : (_ t, Sil.instr, 'a) Container.fold +val foldi : _ t -> init:'a -> f:(int -> 'a -> Sil.instr -> 'a) -> 'a + val iter : (_ t, Sil.instr) Container.iter val get_underlying_not_reversed : not_reversed t -> Sil.instr array diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 06c017a89..820ea4586 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -90,7 +90,7 @@ module type NodeTransferFunctions = sig val exec_node_instrs : Domain.t State.t option - -> exec_instr:(Domain.t -> Sil.instr -> Domain.t) + -> exec_instr:(ProcCfg.InstrNode.instr_index -> Domain.t -> Sil.instr -> Domain.t) -> Domain.t -> _ Instrs.t -> Domain.t @@ -103,7 +103,7 @@ module SimpleNodeTransferFunctions (T : TransferFunctions.SIL) = struct include T let exec_node_instrs _old_state_opt ~exec_instr pre instrs = - Instrs.fold ~init:pre instrs ~f:exec_instr + Instrs.foldi ~init:pre instrs ~f:exec_instr end (** build a disjunctive domain and transfer functions *) @@ -181,7 +181,7 @@ struct F.fprintf f "@[%d disjuncts:@;%a@]" (List.length disjuncts) pp_disjuncts disjuncts end - let exec_instr pre_disjuncts analysis_data node instr = + let exec_instr pre_disjuncts analysis_data node _ instr = List.foldi pre_disjuncts ~init:[] ~f:(fun i post_disjuncts pre_disjunct -> let should_skip = let (`UnderApproximateAfter n) = DConfig.join_policy in @@ -211,7 +211,7 @@ struct List.foldi pre ~init:current_post ~f:(fun i post_disjuncts pre_disjunct -> if is_new_pre pre_disjunct then ( L.d_printfln "@[Executing node from disjunct #%d@;" i ; - let disjuncts' = Instrs.fold ~init:[pre_disjunct] instrs ~f:exec_instr in + let disjuncts' = Instrs.foldi ~init:[pre_disjunct] instrs ~f:exec_instr in L.d_printfln "@]@\n" ; Domain.join post_disjuncts disjuncts' ) else ( @@ -294,11 +294,11 @@ module AbstractInterpreterCommon (TransferFunctions : NodeTransferFunctions) = s let exec_node_instrs old_state_opt ~pp_instr proc_data node pre = let instrs = CFG.instrs node in if Config.write_html then L.d_printfln_escaped "PRE STATE:@\n@[%a@]@\n" Domain.pp pre ; - let exec_instr pre instr = + let exec_instr idx pre instr = AnalysisState.set_instr instr ; let result = try - let post = TransferFunctions.exec_instr pre proc_data node instr in + let post = TransferFunctions.exec_instr pre proc_data node idx instr in (* don't forget to reset this so we output messages for future errors too *) logged_error := false ; Ok post diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml index 563226aed..3188b684e 100644 --- a/infer/src/absint/LowerHil.ml +++ b/infer/src/absint/LowerHil.ml @@ -40,7 +40,7 @@ module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig) && match ConcurrencyModels.get_lock_effect pname actuals with Unlock _ -> true | _ -> false - let exec_instr_actual analysis_data bindings node hil_instr actual_state = + let exec_instr_actual analysis_data bindings node idx hil_instr actual_state = match (hil_instr : HilInstr.t) with | Call (_, Direct callee_pname, actuals, _, loc) as hil_instr when is_java_unlock callee_pname actuals -> @@ -53,11 +53,11 @@ module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig) let dummy_assign = HilInstr.Assign (lhs_access_path, HilExp.AccessExpression access_expr, loc) in - TransferFunctions.exec_instr astate_acc analysis_data node dummy_assign ) + TransferFunctions.exec_instr astate_acc analysis_data node idx dummy_assign ) in - (TransferFunctions.exec_instr actual_state' analysis_data node hil_instr, Bindings.empty) + (TransferFunctions.exec_instr actual_state' analysis_data node idx hil_instr, Bindings.empty) | hil_instr -> - (TransferFunctions.exec_instr actual_state analysis_data node hil_instr, bindings) + (TransferFunctions.exec_instr actual_state analysis_data node idx hil_instr, bindings) let append_bindings = IList.append_no_duplicates ~cmp:Var.compare |> Staged.unstage @@ -84,13 +84,13 @@ module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig) (Some instr, bindings) - let exec_instr ((actual_state, bindings) as astate) analysis_data node instr = + let exec_instr ((actual_state, bindings) as astate) analysis_data node idx instr = let actual_state', bindings' = match hil_instr_of_sil bindings instr with | None, bindings -> (actual_state, bindings) | Some hil_instr, bindings -> - exec_instr_actual analysis_data bindings node hil_instr actual_state + exec_instr_actual analysis_data bindings node idx hil_instr actual_state in if phys_equal bindings bindings' && phys_equal actual_state actual_state' then astate else (actual_state', bindings') diff --git a/infer/src/absint/LowerHil.mli b/infer/src/absint/LowerHil.mli index bf1407a8e..ab96816d7 100644 --- a/infer/src/absint/LowerHil.mli +++ b/infer/src/absint/LowerHil.mli @@ -29,7 +29,13 @@ module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig) type analysis_data = TransferFunctions.analysis_data - val exec_instr : Domain.t -> analysis_data -> CFG.Node.t -> Sil.instr -> Domain.t + val exec_instr : + Domain.t + -> analysis_data + -> CFG.Node.t + -> ProcCfg.InstrNode.instr_index + -> Sil.instr + -> Domain.t val pp_session_name : CFG.Node.t -> Format.formatter -> unit end diff --git a/infer/src/absint/ProcCfg.ml b/infer/src/absint/ProcCfg.ml index c423d2da7..28b7ed92d 100644 --- a/infer/src/absint/ProcCfg.ml +++ b/infer/src/absint/ProcCfg.ml @@ -12,7 +12,7 @@ module F = Format file). Defines useful wrappers that allows us to do tricks like turn a forward cfg into a backward one, or view a cfg as having a single instruction per node. *) -module type Node = sig +module type NodeCommonS = sig type t type id @@ -38,26 +38,37 @@ module type Node = sig module IdSet : PrettyPrintable.PPSet with type elt = id end -module DefaultNode : Node with type t = Procdesc.Node.t and type id = Procdesc.Node.id = struct - type t = Procdesc.Node.t +module InstrNode : sig + type instr_index = int - type id = Procdesc.Node.id + include + NodeCommonS + with type t = Procdesc.Node.t * instr_index + and type id = Procdesc.Node.id * instr_index - let kind = Procdesc.Node.get_kind + val compare : t -> t -> int - let id = Procdesc.Node.get_id + val to_instr : instr_index -> t -> t +end = struct + type instr_index = int [@@deriving compare] - let hash = Procdesc.Node.hash + type t = Procdesc.Node.t * instr_index [@@deriving compare] - let loc = Procdesc.Node.get_loc + type id = Procdesc.Node.id * instr_index [@@deriving compare] - let underlying_node t = t + let kind (t, _) = Procdesc.Node.get_kind t - let of_underlying_node t = t + let underlying_node (t, _) = t - let compare_id = Procdesc.Node.compare_id + let of_underlying_node t = (t, 0) - let pp_id = Procdesc.Node.pp_id + let id (t, index) = (Procdesc.Node.get_id t, index) + + let hash node = Hashtbl.hash (id node) + + let loc (t, _) = Procdesc.Node.get_loc t + + let pp_id fmt (id, index) = F.fprintf fmt "(%a: %d)" Procdesc.Node.pp_id id index module OrderedId = struct type t = id [@@deriving compare] @@ -65,35 +76,38 @@ module DefaultNode : Node with type t = Procdesc.Node.t and type id = Procdesc.N let pp = pp_id end - module IdMap = Procdesc.IdMap + module IdMap = PrettyPrintable.MakePPMap (OrderedId) module IdSet = PrettyPrintable.MakePPSet (OrderedId) + + let to_instr _ t = t end -module InstrNode : sig - type instr_index = int +module type Node = sig + include NodeCommonS - include - Node with type t = Procdesc.Node.t * instr_index and type id = Procdesc.Node.id * instr_index -end = struct - type instr_index = int [@@deriving compare] + val to_instr : InstrNode.instr_index -> t -> InstrNode.t +end - type t = Procdesc.Node.t * instr_index +module DefaultNode : Node with type t = Procdesc.Node.t and type id = Procdesc.Node.id = struct + type t = Procdesc.Node.t - type id = Procdesc.Node.id * instr_index [@@deriving compare] + type id = Procdesc.Node.id - let kind (t, _) = Procdesc.Node.get_kind t + let kind = Procdesc.Node.get_kind - let underlying_node (t, _) = t + let id = Procdesc.Node.get_id - let of_underlying_node t = (t, 0) + let hash = Procdesc.Node.hash - let id (t, index) = (Procdesc.Node.get_id t, index) + let loc = Procdesc.Node.get_loc - let hash node = Hashtbl.hash (id node) + let underlying_node t = t - let loc (t, _) = Procdesc.Node.get_loc t + let of_underlying_node t = t - let pp_id fmt (id, index) = F.fprintf fmt "(%a: %d)" Procdesc.Node.pp_id id index + let compare_id = Procdesc.Node.compare_id + + let pp_id = Procdesc.Node.pp_id module OrderedId = struct type t = id [@@deriving compare] @@ -101,8 +115,10 @@ end = struct let pp = pp_id end - module IdMap = PrettyPrintable.MakePPMap (OrderedId) + module IdMap = Procdesc.IdMap module IdSet = PrettyPrintable.MakePPSet (OrderedId) + + let to_instr index node = (node, index) end module type S = sig @@ -325,8 +341,6 @@ module OneInstrPerNode (Base : S with module Node = DefaultNode) : sig S with type t = Base.t and module Node = InstrNode and type instrs_dir = Instrs.not_reversed val last_of_underlying_node : Procdesc.Node.t -> Node.t - - val of_instr_opt : Procdesc.Node.t -> Sil.instr -> Node.t option end = struct type t = Base.t @@ -343,11 +357,6 @@ end = struct let last_of_node node = (node, max 0 (Instrs.count (Base.instrs node) - 1)) - let of_instr_opt node instr = - let instrs = Procdesc.Node.get_instrs node in - Instrs.find_instr_index instrs instr |> Option.map ~f:(fun index -> (node, index)) - - let last_of_underlying_node = last_of_node let fold_normal_succs _ _ ~init:_ ~f:_ = (* not used *) assert false diff --git a/infer/src/absint/ProcCfg.mli b/infer/src/absint/ProcCfg.mli index a059bdc5e..77677531c 100644 --- a/infer/src/absint/ProcCfg.mli +++ b/infer/src/absint/ProcCfg.mli @@ -11,7 +11,7 @@ open! IStd file). Defines useful wrappers that allows us to do tricks like turn a forward cfg to into a backward one, or view a cfg as having a single instruction per block *) -module type Node = sig +module type NodeCommonS = sig type t type id @@ -37,6 +37,26 @@ module type Node = sig module IdSet : PrettyPrintable.PPSet with type elt = id end +module InstrNode : sig + (* NOTE: The type is not abstracted since it is used in the [Instrs] module. *) + type instr_index = int + + include + NodeCommonS + with type t = Procdesc.Node.t * instr_index + and type id = Procdesc.Node.id * instr_index + + val compare : t -> t -> int + + val to_instr : instr_index -> t -> t +end + +module type Node = sig + include NodeCommonS + + val to_instr : InstrNode.instr_index -> t -> InstrNode.t +end + module type S = sig type t @@ -82,13 +102,6 @@ end module DefaultNode : Node with type t = Procdesc.Node.t and type id = Procdesc.Node.id -module InstrNode : sig - type instr_index - - include - Node with type t = Procdesc.Node.t * instr_index and type id = Procdesc.Node.id * instr_index -end - (** Forward CFG with no exceptional control-flow *) module Normal : S with type t = Procdesc.t and module Node = DefaultNode and type instrs_dir = Instrs.not_reversed @@ -109,8 +122,6 @@ module OneInstrPerNode (Base : S with module Node = DefaultNode) : sig S with type t = Base.t and module Node = InstrNode and type instrs_dir = Instrs.not_reversed val last_of_underlying_node : Procdesc.Node.t -> Node.t - - val of_instr_opt : Procdesc.Node.t -> Sil.instr -> Node.t option end module NormalOneInstrPerNode : module type of OneInstrPerNode (Normal) diff --git a/infer/src/absint/TransferFunctions.ml b/infer/src/absint/TransferFunctions.ml index 954197c7c..544d0430e 100644 --- a/infer/src/absint/TransferFunctions.ml +++ b/infer/src/absint/TransferFunctions.ml @@ -16,7 +16,8 @@ module type S = sig type instr - val exec_instr : Domain.t -> analysis_data -> CFG.Node.t -> instr -> Domain.t + val exec_instr : + Domain.t -> analysis_data -> CFG.Node.t -> ProcCfg.InstrNode.instr_index -> instr -> Domain.t val pp_session_name : CFG.Node.t -> Format.formatter -> unit end diff --git a/infer/src/absint/TransferFunctions.mli b/infer/src/absint/TransferFunctions.mli index e6482f508..7715b2727 100644 --- a/infer/src/absint/TransferFunctions.mli +++ b/infer/src/absint/TransferFunctions.mli @@ -22,12 +22,13 @@ module type S = sig (** type of the instructions the transfer functions operate on *) type instr - val exec_instr : Domain.t -> analysis_data -> CFG.Node.t -> instr -> Domain.t - (** [exec_instr astate proc_data node instr] should usually return [astate'] such that + val exec_instr : + Domain.t -> analysis_data -> CFG.Node.t -> ProcCfg.InstrNode.instr_index -> instr -> Domain.t + (** [exec_instr astate proc_data node idx instr] should usually return [astate'] such that [{astate} instr {astate'}] is a valid Hoare triple. In other words, [exec_instr] defines how executing an instruction from a given abstract state changes that state into a new one. This is usually called the {i transfer function} in Abstract Interpretation terms. [node] is the - node containing the current instruction. *) + node containing the current instruction and [idx] is the index of the instruction in the node. *) val pp_session_name : CFG.Node.t -> Format.formatter -> unit (** print session name for HTML debug *) diff --git a/infer/src/backend/ClosureSubstSpecializedMethod.ml b/infer/src/backend/ClosureSubstSpecializedMethod.ml index 0de03de11..e4e777824 100644 --- a/infer/src/backend/ClosureSubstSpecializedMethod.ml +++ b/infer/src/backend/ClosureSubstSpecializedMethod.ml @@ -58,7 +58,7 @@ module TransferFunctions = struct type analysis_data = unit - let exec_instr astate _ _node instr = eval_instr astate instr + let exec_instr astate _ _node _ instr = eval_instr astate instr let pp_session_name node fmt = Format.fprintf fmt "Closure Subst Specialized Method %a" CFG.Node.pp_id (CFG.Node.id node) diff --git a/infer/src/backend/ClosuresSubstitution.ml b/infer/src/backend/ClosuresSubstitution.ml index a90f1b607..df759991f 100644 --- a/infer/src/backend/ClosuresSubstitution.ml +++ b/infer/src/backend/ClosuresSubstitution.ml @@ -67,7 +67,7 @@ module TransferFunctions = struct type analysis_data = unit - let exec_instr astate _ _node instr = eval_instr astate instr + let exec_instr astate _ _node _ instr = eval_instr astate instr let pp_session_name node fmt = Format.fprintf fmt "Closures Substitution %a" CFG.Node.pp_id (CFG.Node.id node) diff --git a/infer/src/backend/Devirtualizer.ml b/infer/src/backend/Devirtualizer.ml index a678889b9..7564bf643 100644 --- a/infer/src/backend/Devirtualizer.ml +++ b/infer/src/backend/Devirtualizer.ml @@ -80,7 +80,7 @@ module TransferFunctions = struct type analysis_data = unit - let exec_instr astate _ _node instr = eval_instr astate instr + let exec_instr astate _ _node _ instr = eval_instr astate instr let pp_session_name node fmt = Format.fprintf fmt "devirtualizer analysis %a" CFG.Node.pp_id (CFG.Node.id node) diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index 7e180fa42..f79b3bfd1 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -326,7 +326,7 @@ module Liveness = struct let is_last_instr_in_node instr node = phys_equal (last_instr_in_node node) instr - let exec_instr ((active_defs, to_nullify) as astate) extras node instr = + let exec_instr ((active_defs, to_nullify) as astate) extras node _ instr = let astate' = match instr with | Sil.Load {id= lhs_id} -> diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index 00392adb1..47986fefa 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -314,10 +314,16 @@ module TransferFunctions = struct Dom.Mem.add_unknown ret ~location mem - let exec_instr : Dom.Mem.t -> analysis_data -> CFG.Node.t -> Sil.instr -> Dom.Mem.t = + let exec_instr : + Dom.Mem.t + -> analysis_data + -> CFG.Node.t + -> ProcCfg.InstrNode.instr_index + -> Sil.instr + -> Dom.Mem.t = fun mem ({interproc= {proc_desc; tenv}; get_summary; oenv= {integer_type_widths}} as analysis_data) - node instr -> + node _ instr -> match instr with | Load {id} when Ident.is_none id -> mem diff --git a/infer/src/checkers/ConfigChecksBetweenMarkers.ml b/infer/src/checkers/ConfigChecksBetweenMarkers.ml index ecea1828a..f019f7173 100644 --- a/infer/src/checkers/ConfigChecksBetweenMarkers.ml +++ b/infer/src/checkers/ConfigChecksBetweenMarkers.ml @@ -577,7 +577,7 @@ module TransferFunctions = struct let exec_instr ({Dom.mem} as astate) - ({InterproceduralAnalysis.tenv; analyze_dependency} as analysis_data) _node instr = + ({InterproceduralAnalysis.tenv; analyze_dependency} as analysis_data) _node _ instr = match (instr : Sil.instr) with | Load {id; e= Lvar pvar} -> Dom.load_config id pvar astate diff --git a/infer/src/checkers/NullabilityPreanalysis.ml b/infer/src/checkers/NullabilityPreanalysis.ml index 53f1a4d1f..58b9a7ad6 100644 --- a/infer/src/checkers/NullabilityPreanalysis.ml +++ b/infer/src/checkers/NullabilityPreanalysis.ml @@ -38,7 +38,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct with Caml.Not_found -> false - let exec_instr astate id_table _ instr = + let exec_instr astate id_table _ _ instr = match instr with | Sil.Load {id; e= exp} -> Ident.Hash.add id_table id exp ; diff --git a/infer/src/checkers/PurityAnalysis.ml b/infer/src/checkers/PurityAnalysis.ml index 98c47a249..dc3699d42 100644 --- a/infer/src/checkers/PurityAnalysis.ml +++ b/infer/src/checkers/PurityAnalysis.ml @@ -143,7 +143,7 @@ module TransferFunctions = struct let modified_global ae = HilExp.AccessExpression.get_base ae |> fst |> Var.is_global let exec_instr (astate : Domain.t) {tenv; inferbo_invariant_map; formals; get_callee_summary} - (node : CFG.Node.t) (instr : HilInstr.t) = + (node : CFG.Node.t) _ (instr : HilInstr.t) = let (node_id : InstrCFG.Node.id) = CFG.Node.underlying_node node |> InstrCFG.last_of_underlying_node |> InstrCFG.Node.id in diff --git a/infer/src/checkers/RequiredProps.ml b/infer/src/checkers/RequiredProps.ml index 27ad8e79c..ba438494b 100644 --- a/infer/src/checkers/RequiredProps.ml +++ b/infer/src/checkers/RequiredProps.ml @@ -211,7 +211,7 @@ module TransferFunctions = struct Domain.assume_null access_path astate - let exec_instr astate {interproc= {proc_desc; tenv}; get_proc_summary_and_formals} _ + let exec_instr astate {interproc= {proc_desc; tenv}; get_proc_summary_and_formals} _ _ (instr : HilInstr.t) : Domain.t = let caller_pname = Procdesc.get_proc_name proc_desc in match instr with diff --git a/infer/src/checkers/SelfInBlock.ml b/infer/src/checkers/SelfInBlock.ml index f7eac8536..85d87411a 100644 --- a/infer/src/checkers/SelfInBlock.ml +++ b/infer/src/checkers/SelfInBlock.ml @@ -343,7 +343,7 @@ module TransferFunctions = struct report_on_non_nullable_arg ?annotations domain args - let exec_instr (astate : Domain.t) {IntraproceduralAnalysis.proc_desc; err_log} _cfg_node + let exec_instr (astate : Domain.t) {IntraproceduralAnalysis.proc_desc; err_log} _cfg_node _ (instr : Sil.instr) = let attributes = Procdesc.get_attributes proc_desc in let astate = report_unchecked_strongself_issues_on_exps proc_desc err_log astate instr in diff --git a/infer/src/checkers/Siof.ml b/infer/src/checkers/Siof.ml index 0c4d82346..28c78934b 100644 --- a/infer/src/checkers/Siof.ml +++ b/infer/src/checkers/Siof.ml @@ -129,7 +129,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let at_least_nonbottom = Domain.join (NonBottom SiofTrace.bottom, Domain.VarNames.empty) let exec_instr astate - ({InterproceduralAnalysis.proc_desc; analyze_dependency; _} as analysis_data) _ + ({InterproceduralAnalysis.proc_desc; analyze_dependency; _} as analysis_data) _ _ (instr : Sil.instr) = match instr with | Store {e1= Lvar global; typ= Typ.{desc= Tptr _}; e2= Lvar _; loc} diff --git a/infer/src/checkers/addressTaken.ml b/infer/src/checkers/addressTaken.ml index 6fa38d068..9b333fbe2 100644 --- a/infer/src/checkers/addressTaken.ml +++ b/infer/src/checkers/addressTaken.ml @@ -35,7 +35,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct astate - let exec_instr astate () _ = function + let exec_instr astate () _ _ = function | Sil.Store {typ= {desc= Tptr _}; e2= rhs_exp} -> add_address_taken_pvars rhs_exp astate | Sil.Call (_, _, actuals, _, _) -> diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index 96719b934..08d7b5840 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -533,7 +533,7 @@ module MakeTransferFunctions (CFG : ProcCfg.S) = struct callee_call_map astate - let exec_instr astate ({analysis_data= {proc_desc; tenv}; specs} as analysis_data) _ = function + let exec_instr astate ({analysis_data= {proc_desc; tenv}; specs} as analysis_data) _ _ = function | Sil.Call (_, Const (Cfun callee_pname), _, call_loc, _) -> let caller_pname = Procdesc.get_proc_name proc_desc in let call_site = CallSite.make callee_pname call_loc in diff --git a/infer/src/checkers/control.ml b/infer/src/checkers/control.ml index cb3a572e6..d4e42f2b0 100644 --- a/infer/src/checkers/control.ml +++ b/infer/src/checkers/control.ml @@ -133,7 +133,7 @@ module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct along with the loop header that CV is originating from - a loop exit node, remove control variables of its guard nodes This is correct because the CVs are only going to be temporaries. *) - let exec_instr astate (nodes, {exit_map; loop_head_to_guard_nodes}) (node : CFG.Node.t) _ = + let exec_instr astate (nodes, {exit_map; loop_head_to_guard_nodes}) (node : CFG.Node.t) _ _ = let node = CFG.Node.underlying_node node in let astate' = match LoopHeadToGuardNodes.find_opt node loop_head_to_guard_nodes with diff --git a/infer/src/checkers/functionPointers.ml b/infer/src/checkers/functionPointers.ml index d36b21919..fc7632583 100644 --- a/infer/src/checkers/functionPointers.ml +++ b/infer/src/checkers/functionPointers.ml @@ -16,7 +16,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct type analysis_data = unit - let exec_instr astate () _ = function + let exec_instr astate () _ _ = function | Sil.Load {id= lhs_id} when Ident.is_none lhs_id -> astate | Sil.Load {id= lhs_id; e= Exp.Lvar rhs_pvar; typ= Typ.{desc= Tptr ({desc= Tfun}, _)}} -> diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml index 48b3eaf4e..14e3c8807 100644 --- a/infer/src/checkers/liveness.ml +++ b/infer/src/checkers/liveness.ml @@ -183,7 +183,7 @@ module TransferFunctions (LConfig : LivenessConfig) (CFG : ProcCfg.S) = struct List.fold actuals ~f:(fun acc_ exp -> exp_add_live exp acc_) ~init:live_acc - let exec_instr astate proc_desc _ = function + let exec_instr astate proc_desc _ _ = function | Sil.Load {id= lhs_id} when Ident.is_none lhs_id -> (* dummy deref inserted by frontend--don't count as a read *) astate @@ -268,7 +268,7 @@ module PassedByRefTransferFunctions (CFG : ProcCfg.S) = struct proc_name_of_expr expr |> Option.exists ~f:CheckerMode.is_dangerous_proc_name - let exec_instr astate () _ (instr : Sil.instr) = + let exec_instr astate () _ _ (instr : Sil.instr) = let astate = match instr with | Call (_ret, f, actuals, _loc, _flags) when not (is_dangerous f) -> diff --git a/infer/src/checkers/reachingDefs.ml b/infer/src/checkers/reachingDefs.ml index b329fc126..df458db71 100644 --- a/infer/src/checkers/reachingDefs.ml +++ b/infer/src/checkers/reachingDefs.ml @@ -27,7 +27,7 @@ module TransferFunctionsReachingDefs (CFG : ProcCfg.S) = struct type analysis_data = unit (* for each x := e at node n, remove x's definitions and introduce x -> n *) - let exec_instr astate () (node : CFG.Node.t) instr = + let exec_instr astate () (node : CFG.Node.t) _ instr = let node = CFG.Node.underlying_node node in let strong_update_def astate var = Domain.add var (Defs.singleton node) astate in let weak_update_def astate var = diff --git a/infer/src/checkers/uninit.ml b/infer/src/checkers/uninit.ml index 20d272693..cdd367eb6 100644 --- a/infer/src/checkers/uninit.ml +++ b/infer/src/checkers/uninit.ml @@ -209,7 +209,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let exec_instr (astate : Domain.t) {analysis_data= {proc_desc; tenv} as analysis_data; formals} _ - (instr : HilInstr.t) = + _ (instr : HilInstr.t) = let check_access_expr ~loc rhs_access_expr = if should_report_var proc_desc tenv astate.maybe_uninit_vars rhs_access_expr then report_intra rhs_access_expr loc analysis_data diff --git a/infer/src/concurrency/RacerDProcAnalysis.ml b/infer/src/concurrency/RacerDProcAnalysis.ml index a65cf1bee..f2a572a2d 100644 --- a/infer/src/concurrency/RacerDProcAnalysis.ml +++ b/infer/src/concurrency/RacerDProcAnalysis.ml @@ -195,7 +195,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct astate - let exec_instr astate ({interproc= {proc_desc; tenv}; formals} as analysis_data) _ instr = + let exec_instr astate ({interproc= {proc_desc; tenv}; formals} as analysis_data) _ _ instr = match (instr : HilInstr.t) with | Call (ret_base, Direct callee_pname, actuals, call_flags, loc) -> let astate = Domain.add_reads_of_hilexps tenv formals actuals loc astate in diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 39ed0719b..5c0cf27e4 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -259,7 +259,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct astate - let exec_instr (astate : Domain.t) ({interproc= {proc_desc; tenv}; formals} as analysis_data) _ + let exec_instr (astate : Domain.t) ({interproc= {proc_desc; tenv}; formals} as analysis_data) _ _ instr = let open ConcurrencyModels in let open StarvationModels in diff --git a/infer/src/cost/ConfigImpactAnalysis.ml b/infer/src/cost/ConfigImpactAnalysis.ml index b02c7b875..daf74c9fd 100644 --- a/infer/src/cost/ConfigImpactAnalysis.ml +++ b/infer/src/cost/ConfigImpactAnalysis.ml @@ -482,7 +482,7 @@ module TransferFunctions = struct fun tenv pname -> dispatch tenv pname |> Option.is_some - let exec_instr astate {interproc= {tenv; analyze_dependency}; get_is_cheap_call} node instr = + let exec_instr astate {interproc= {tenv; analyze_dependency}; get_is_cheap_call} node idx instr = match (instr : Sil.instr) with | Load {id; e= Lvar pvar} -> Dom.load_config id pvar astate @@ -505,7 +505,10 @@ module TransferFunctions = struct astate | None -> (* normal function calls *) - let call = CostInstantiate.Call.{instr; loc= location; pname= callee; node; args; ret} in + let call = + CostInstantiate.Call. + {loc= location; pname= callee; node= CFG.Node.to_instr idx node; args; ret} + in let is_cheap_call = get_is_cheap_call call in Dom.call tenv analyze_dependency ~is_cheap_call callee args location astate ) | Prune (e, _, _, _) -> diff --git a/infer/src/cost/costInstantiate.ml b/infer/src/cost/costInstantiate.ml index 863515968..0a2372fae 100644 --- a/infer/src/cost/costInstantiate.ml +++ b/infer/src/cost/costInstantiate.ml @@ -6,14 +6,12 @@ *) open! IStd module F = Format -module InstrCFG = ProcCfg.NormalOneInstrPerNode module Call = struct type t = - { instr: Sil.instr - ; loc: Location.t + { loc: Location.t ; pname: Procname.t - ; node: Procdesc.Node.t + ; node: ProcCfg.InstrNode.t ; args: (Exp.t * Typ.t) list ; ret: Ident.t * Typ.t } [@@deriving compare] @@ -40,13 +38,12 @@ let get_symbolic_cost ; get_callee_cost_summary_and_formals ; inferbo_invariant_map ; inferbo_get_summary - ; call= Call.{instr; pname; node; ret; args} } = - let last_node = Option.value_exn (InstrCFG.of_instr_opt node instr) in + ; call= Call.{pname; node; ret; args} } = let inferbo_mem = - let instr_node_id = InstrCFG.Node.id last_node in - Option.value_exn (BufferOverrunAnalysis.extract_pre instr_node_id inferbo_invariant_map) + Option.value_exn + (BufferOverrunAnalysis.extract_pre (ProcCfg.InstrNode.id node) inferbo_invariant_map) in - let loc = InstrCFG.Node.loc last_node in + let loc = ProcCfg.InstrNode.loc node in let get_symbolic cost = if CostDomain.BasicCost.is_symbolic cost then `SymbolicCost cost else `Cheap in @@ -68,7 +65,7 @@ let get_symbolic_cost CostModels.Call.dispatch tenv pname fun_arg_list |> Option.value_map ~default:`NoModel ~f:(fun model -> let model_env = - let node_hash = InstrCFG.Node.hash last_node in + let node_hash = ProcCfg.InstrNode.hash node in BufferOverrunUtils.ModelEnv.mk_model_env pname ~node_hash loc tenv integer_type_widths inferbo_get_summary in diff --git a/infer/src/cost/costInstantiate.mli b/infer/src/cost/costInstantiate.mli index 0b04db2d9..f87ee2b9e 100644 --- a/infer/src/cost/costInstantiate.mli +++ b/infer/src/cost/costInstantiate.mli @@ -9,10 +9,9 @@ open! IStd module Call : sig type t = - { instr: Sil.instr - ; loc: Location.t + { loc: Location.t ; pname: Procname.t - ; node: Procdesc.Node.t + ; node: ProcCfg.InstrNode.t ; args: (Exp.t * Typ.t) list ; ret: Ident.t * Typ.t } [@@deriving compare] diff --git a/infer/src/cost/hoisting.ml b/infer/src/cost/hoisting.ml index 6ca0e35c1..f1f2e2b2e 100644 --- a/infer/src/cost/hoisting.ml +++ b/infer/src/cost/hoisting.ml @@ -19,14 +19,16 @@ module LoopHeadToHoistInstrs = Procdesc.NodeMap * 1. C is guaranteed to execute, i.e. N dominates all loop sources * 2. args are loop invariant *) -let add_if_hoistable inv_vars instr node source_nodes idom hoistable_calls = +let add_if_hoistable inv_vars instr node idx source_nodes idom hoistable_calls = match instr with | Sil.Call (((ret_id, _) as ret), Exp.Const (Const.Cfun pname), args, loc, _) when (* Check condition (1); N dominates all loop sources *) List.for_all ~f:(fun source -> Dominators.dominates idom node source) source_nodes && (* Check condition (2); id should be invariant already *) LoopInvariant.InvariantVars.mem (Var.of_id ret_id) inv_vars -> - HoistCalls.add {instr; pname; loc; node; args; ret} hoistable_calls + HoistCalls.add + {pname; loc; node= ProcCfg.DefaultNode.to_instr idx node; args; ret} + hoistable_calls | _ -> hoistable_calls @@ -35,8 +37,8 @@ let get_hoistable_calls inv_vars loop_nodes source_nodes idom = LoopNodes.fold (fun node hoist_calls -> let instr_in_node = Procdesc.Node.get_instrs node in - Instrs.fold ~init:hoist_calls - ~f:(fun acc instr -> add_if_hoistable inv_vars instr node source_nodes idom acc) + Instrs.foldi ~init:hoist_calls + ~f:(fun idx acc instr -> add_if_hoistable inv_vars instr node idx source_nodes idom acc) instr_in_node ) loop_nodes HoistCalls.empty diff --git a/infer/src/dotnet/ResourceLeaksCS.ml b/infer/src/dotnet/ResourceLeaksCS.ml index 41a192584..c351d019c 100644 --- a/infer/src/dotnet/ResourceLeaksCS.ml +++ b/infer/src/dotnet/ResourceLeaksCS.ml @@ -61,7 +61,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (** Take an abstract state and instruction, produce a new abstract state *) let exec_instr (astate : ResourceLeakCSDomain.t) - {InterproceduralAnalysis.proc_desc; tenv; analyze_dependency; _} _ (instr : HilInstr.t) = + {InterproceduralAnalysis.proc_desc; tenv; analyze_dependency; _} _ _ (instr : HilInstr.t) = let assign_type_map = type_map := ResourceLeakCSDomain.get_type_map in assign_type_map ; let is_not_enumerable = diff --git a/infer/src/labs/00_dummy_checker/ResourceLeaks.ml b/infer/src/labs/00_dummy_checker/ResourceLeaks.ml index 12174047b..ee1c18d04 100644 --- a/infer/src/labs/00_dummy_checker/ResourceLeaks.ml +++ b/infer/src/labs/00_dummy_checker/ResourceLeaks.ml @@ -46,7 +46,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (** Take an abstract state and instruction, produce a new abstract state *) let exec_instr (astate : ResourceLeakDomain.t) - {InterproceduralAnalysis.proc_desc= _; tenv= _; analyze_dependency= _; _} _ + {InterproceduralAnalysis.proc_desc= _; tenv= _; analyze_dependency= _; _} _ _ (instr : HilInstr.t) = match instr with | Call (_return_opt, Direct _callee_procname, _actuals, _, _loc) -> diff --git a/infer/src/labs/01_integer_domain/ResourceLeaks.ml b/infer/src/labs/01_integer_domain/ResourceLeaks.ml index b702f2089..8479d64ea 100644 --- a/infer/src/labs/01_integer_domain/ResourceLeaks.ml +++ b/infer/src/labs/01_integer_domain/ResourceLeaks.ml @@ -46,8 +46,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (** Take an abstract state and instruction, produce a new abstract state *) let exec_instr (astate : ResourceLeakDomain.t) - {InterproceduralAnalysis.proc_desc= _; tenv; analyze_dependency= _; _} _ (instr : HilInstr.t) - = + {InterproceduralAnalysis.proc_desc= _; tenv; analyze_dependency= _; _} _ _ + (instr : HilInstr.t) = match instr with | Call (_return_opt, Direct callee_procname, _actuals, _, _loc) -> (* function call [return_opt] := invoke [callee_procname]([actuals]) *) diff --git a/infer/src/labs/02_domain_join/ResourceLeaks.ml b/infer/src/labs/02_domain_join/ResourceLeaks.ml index b702f2089..8479d64ea 100644 --- a/infer/src/labs/02_domain_join/ResourceLeaks.ml +++ b/infer/src/labs/02_domain_join/ResourceLeaks.ml @@ -46,8 +46,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (** Take an abstract state and instruction, produce a new abstract state *) let exec_instr (astate : ResourceLeakDomain.t) - {InterproceduralAnalysis.proc_desc= _; tenv; analyze_dependency= _; _} _ (instr : HilInstr.t) - = + {InterproceduralAnalysis.proc_desc= _; tenv; analyze_dependency= _; _} _ _ + (instr : HilInstr.t) = match instr with | Call (_return_opt, Direct callee_procname, _actuals, _, _loc) -> (* function call [return_opt] := invoke [callee_procname]([actuals]) *) diff --git a/infer/src/labs/03_domain_top/ResourceLeaks.ml b/infer/src/labs/03_domain_top/ResourceLeaks.ml index b702f2089..8479d64ea 100644 --- a/infer/src/labs/03_domain_top/ResourceLeaks.ml +++ b/infer/src/labs/03_domain_top/ResourceLeaks.ml @@ -46,8 +46,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (** Take an abstract state and instruction, produce a new abstract state *) let exec_instr (astate : ResourceLeakDomain.t) - {InterproceduralAnalysis.proc_desc= _; tenv; analyze_dependency= _; _} _ (instr : HilInstr.t) - = + {InterproceduralAnalysis.proc_desc= _; tenv; analyze_dependency= _; _} _ _ + (instr : HilInstr.t) = match instr with | Call (_return_opt, Direct callee_procname, _actuals, _, _loc) -> (* function call [return_opt] := invoke [callee_procname]([actuals]) *) diff --git a/infer/src/labs/04_interprocedural/ResourceLeaks.ml b/infer/src/labs/04_interprocedural/ResourceLeaks.ml index a67169802..0bbb70e30 100644 --- a/infer/src/labs/04_interprocedural/ResourceLeaks.ml +++ b/infer/src/labs/04_interprocedural/ResourceLeaks.ml @@ -46,7 +46,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (** Take an abstract state and instruction, produce a new abstract state *) let exec_instr (astate : ResourceLeakDomain.t) - {InterproceduralAnalysis.proc_desc= _; tenv; analyze_dependency; _} _ (instr : HilInstr.t) = + {InterproceduralAnalysis.proc_desc= _; tenv; analyze_dependency; _} _ _ (instr : HilInstr.t) = match instr with | Call (_return_opt, Direct callee_procname, _actuals, _, _loc) -> ( if diff --git a/infer/src/labs/05_access_paths_interprocedural/ResourceLeaks.ml b/infer/src/labs/05_access_paths_interprocedural/ResourceLeaks.ml index 335a463a1..99c320626 100644 --- a/infer/src/labs/05_access_paths_interprocedural/ResourceLeaks.ml +++ b/infer/src/labs/05_access_paths_interprocedural/ResourceLeaks.ml @@ -46,7 +46,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (** Take an abstract state and instruction, produce a new abstract state *) let exec_instr (astate : ResourceLeakDomain.t) - {InterproceduralAnalysis.proc_desc= _; tenv; analyze_dependency; _} _ (instr : HilInstr.t) = + {InterproceduralAnalysis.proc_desc= _; tenv; analyze_dependency; _} _ _ (instr : HilInstr.t) = match instr with | Call (_return, Direct callee_procname, HilExp.AccessExpression allocated :: _, _, _loc) when acquires_resource tenv callee_procname -> diff --git a/infer/src/labs/ResourceLeaks.ml b/infer/src/labs/ResourceLeaks.ml index 12174047b..ee1c18d04 100644 --- a/infer/src/labs/ResourceLeaks.ml +++ b/infer/src/labs/ResourceLeaks.ml @@ -46,7 +46,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (** Take an abstract state and instruction, produce a new abstract state *) let exec_instr (astate : ResourceLeakDomain.t) - {InterproceduralAnalysis.proc_desc= _; tenv= _; analyze_dependency= _; _} _ + {InterproceduralAnalysis.proc_desc= _; tenv= _; analyze_dependency= _; _} _ _ (instr : HilInstr.t) = match instr with | Call (_return_opt, Direct _callee_procname, _actuals, _, _loc) -> diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index 0c22c70af..bd7338866 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -671,7 +671,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct let exec_instr (astate : Domain.t) ({analysis_data= {proc_desc}; formal_map} as analysis_data) _ - (instr : HilInstr.t) = + _ (instr : HilInstr.t) = match instr with | Assign (Base (Var.ProgramVar pvar, _), HilExp.Exception _, _) when Pvar.is_return pvar -> (* the Java frontend translates `throw Exception` as `return Exception`, which is a bit diff --git a/infer/src/unit/abstractInterpreterTests.ml b/infer/src/unit/abstractInterpreterTests.ml index 1840f45ee..5cfe1be3a 100644 --- a/infer/src/unit/abstractInterpreterTests.ml +++ b/infer/src/unit/abstractInterpreterTests.ml @@ -52,7 +52,7 @@ module PathCountTransferFunctions (CFG : ProcCfg.S) = struct type analysis_data = unit (* just propagate the current path count *) - let exec_instr astate _ _ _ = astate + let exec_instr astate _ _ _ _ = astate let pp_session_name _node _fmt = () end diff --git a/infer/src/unit/schedulerTests.ml b/infer/src/unit/schedulerTests.ml index cc9f1f8ef..85c997498 100644 --- a/infer/src/unit/schedulerTests.ml +++ b/infer/src/unit/schedulerTests.ml @@ -38,6 +38,8 @@ module MockNode = struct module IdMap = PrettyPrintable.MakePPMap (OrderedId) module IdSet = PrettyPrintable.MakePPSet (OrderedId) + + let to_instr _ _ = assert false end module MockProcCfg = struct