From 70ed9b146f41ad0875116582df23a0815f90deb4 Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Fri, 19 Oct 2018 07:33:10 -0700 Subject: [PATCH] [classloads] sil version Summary: We don't need the machinery of HIL, or its complexity for this analysis. Reviewed By: ddino Differential Revision: D10461641 fbshipit-source-id: 2e7d3ab8e --- infer/src/concurrency/classLoads.ml | 23 ++++++++-------------- infer/src/concurrency/classLoadsDomain.ml | 2 +- infer/src/concurrency/classLoadsDomain.mli | 2 +- 3 files changed, 10 insertions(+), 17 deletions(-) diff --git a/infer/src/concurrency/classLoads.ml b/infer/src/concurrency/classLoads.ml index 99f300b47..d625cf31e 100644 --- a/infer/src/concurrency/classLoads.ml +++ b/infer/src/concurrency/classLoads.ml @@ -6,7 +6,6 @@ *) open! IStd module F = Format -module L = Logging module Payload = SummaryPayload.Make (struct type t = ClassLoadsDomain.summary @@ -16,17 +15,19 @@ module Payload = SummaryPayload.Make (struct let of_payloads (payloads : Payloads.t) = payloads.class_loads end) -module TransferFunctions (CFG : ProcCfg.S) = struct - module CFG = CFG +module TransferFunctions = struct + module CFG = ProcCfg.Normal module Domain = ClassLoadsDomain type extras = unit - let exec_instr (astate : Domain.astate) {ProcData.pdesc} _ (instr : HilInstr.t) = + type instr = Sil.instr + + let exec_instr (astate : Domain.astate) {ProcData.pdesc} _ (instr : instr) = match instr with - | Call (_, Direct callee, _, _, loc) -> + | Call (_, Const (Cfun callee), _, loc, _) -> Payload.read pdesc callee - |> Option.value_map ~default:astate ~f:(Domain.integrate_summary astate callee loc) + |> Option.fold ~init:astate ~f:(Domain.integrate_summary callee loc) | _ -> astate @@ -34,17 +35,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let pp_session_name _node fmt = F.pp_print_string fmt "class loads" end -module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Normal) (TransferFunctions) - -let die_if_not_java proc_desc = - let is_java = - Procdesc.get_proc_name proc_desc |> Typ.Procname.get_language |> Language.(equal Java) - in - if not is_java then L.(die InternalError "Not supposed to run on non-Java code yet.") - +module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions) let analyze_procedure {Callbacks.proc_desc; tenv; summary} = - die_if_not_java proc_desc ; let initial = ClassLoadsDomain.empty in let proc_data = ProcData.make proc_desc tenv () in Analyzer.compute_post proc_data ~initial diff --git a/infer/src/concurrency/classLoadsDomain.ml b/infer/src/concurrency/classLoadsDomain.ml index 098e28e26..39bf252a4 100644 --- a/infer/src/concurrency/classLoadsDomain.ml +++ b/infer/src/concurrency/classLoadsDomain.ml @@ -21,7 +21,7 @@ let add ({Event.trace} as x) astate = let union xs ys = fold add xs ys -let integrate_summary astate callee_pname loc callee_summary = +let integrate_summary callee_pname loc astate callee_summary = match callee_pname with | Typ.Procname.Java java_pname -> let clazz = Typ.Procname.Java.get_class_name java_pname in diff --git a/infer/src/concurrency/classLoadsDomain.mli b/infer/src/concurrency/classLoadsDomain.mli index 7d2fdec39..83178de83 100644 --- a/infer/src/concurrency/classLoadsDomain.mli +++ b/infer/src/concurrency/classLoadsDomain.mli @@ -13,4 +13,4 @@ type summary = astate val pp_summary : F.formatter -> summary -> unit -val integrate_summary : astate -> Typ.Procname.t -> Location.t -> summary -> astate +val integrate_summary : Typ.Procname.t -> Location.t -> astate -> summary -> astate