From 39ff045569311cde60b5c0c373fd7a82c789c5f3 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Mon, 2 Oct 2017 02:24:12 -0700 Subject: [PATCH] [ai] No need to create a domain for a bottom_lifted type Summary: Makes `type 'astate bottom_lifted` accessible without invoking `BottomLifted` Reviewed By: jvillard, sblackshear Differential Revision: D5920660 fbshipit-source-id: 40fca97 --- infer/src/absint/AbstractDomain.ml | 12 +++++-- infer/src/absint/AbstractDomain.mli | 12 +++++-- .../src/bufferoverrun/bufferOverrunChecker.ml | 3 +- .../src/bufferoverrun/bufferOverrunDomain.ml | 1 + infer/src/bufferoverrun/itv.ml | 1 + infer/src/checkers/Siof.ml | 36 ++++++++----------- infer/src/checkers/SiofDomain.ml | 7 ++-- infer/src/checkers/annotationReachability.ml | 29 +++++++-------- 8 files changed, 54 insertions(+), 47 deletions(-) diff --git a/infer/src/absint/AbstractDomain.ml b/infer/src/absint/AbstractDomain.ml index e51b1e3da..b384d4e98 100644 --- a/infer/src/absint/AbstractDomain.ml +++ b/infer/src/absint/AbstractDomain.ml @@ -10,6 +10,14 @@ open! IStd module F = Format +module Types = struct + type 'astate bottom_lifted = Bottom | NonBottom of 'astate + + type 'astate top_lifted = Top | NonTop of 'astate +end + +open! Types + module type S = sig type astate @@ -39,7 +47,7 @@ module type WithTop = sig end module BottomLifted (Domain : S) = struct - type astate = Bottom | NonBottom of Domain.astate + type astate = Domain.astate bottom_lifted let empty = Bottom @@ -82,7 +90,7 @@ module BottomLifted (Domain : S) = struct end module TopLifted (Domain : S) = struct - type astate = Top | NonTop of Domain.astate + type astate = Domain.astate top_lifted let top = Top diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli index 59b6722d6..dc4831ac0 100644 --- a/infer/src/absint/AbstractDomain.mli +++ b/infer/src/absint/AbstractDomain.mli @@ -10,6 +10,14 @@ open! IStd module F = Format +module Types : sig + type 'astate bottom_lifted = Bottom | NonBottom of 'astate + + type 'astate top_lifted = Top | NonTop of 'astate +end + +open! Types + (** Abstract domains and domain combinators *) module type S = sig @@ -47,14 +55,14 @@ end (** Lift a pre-domain to a domain *) module BottomLifted (Domain : S) : sig - type astate = Bottom | NonBottom of Domain.astate + type astate = Domain.astate bottom_lifted include WithBottom with type astate := astate end (** Create a domain with Top element from a pre-domain *) module TopLifted (Domain : S) : sig - type astate = Top | NonTop of Domain.astate + type astate = Domain.astate top_lifted include WithTop with type astate := astate end diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index ffa43f8c7..0d39ecca2 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -12,6 +12,7 @@ open! IStd open AbsLoc +open! AbstractDomain.Types module F = Format module L = Logging module Dom = BufferOverrunDomain @@ -134,7 +135,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | "__inferbo_min" -> model_min ret params loc mem | "__exit" | "exit" - -> Dom.Mem.Bottom + -> Bottom | "fgetc" -> model_by_value Dom.Val.Itv.m1_255 ret mem | "infer_print" diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 9c2a956c2..8d1985668 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -12,6 +12,7 @@ open! IStd open AbsLoc +open! AbstractDomain.Types module F = Format module L = Logging module MF = MarkupFormatter diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 92019a4e3..0ec3f402c 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -11,6 +11,7 @@ *) open! IStd +open! AbstractDomain.Types module F = Format module L = Logging diff --git a/infer/src/checkers/Siof.ml b/infer/src/checkers/Siof.ml index f776f0e31..22a08aae1 100644 --- a/infer/src/checkers/Siof.ml +++ b/infer/src/checkers/Siof.ml @@ -8,6 +8,7 @@ *) open! IStd +open! AbstractDomain.Types module F = Format module L = Logging module GlobalsAccesses = SiofTrace.GlobalsAccesses @@ -63,7 +64,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let is_compile_time_constructed pdesc pv = let init_pname = Pvar.get_initializer_pname pv in match Option.bind init_pname ~f:(Summary.read_summary pdesc) with - | Some (Domain.BottomSiofTrace.Bottom, _) + | Some (Bottom, _) -> (* we analyzed the initializer for this global and found that it doesn't require any runtime initialization so cannot participate in SIOF *) true @@ -94,13 +95,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let add_globals astate outer_loc globals = if GlobalsAccesses.is_empty globals then astate else - let trace = - match fst astate with - | Domain.BottomSiofTrace.Bottom - -> SiofTrace.empty - | Domain.BottomSiofTrace.NonBottom t - -> t - in + let trace = match fst astate with Bottom -> SiofTrace.empty | NonBottom t -> t in (* filter out variables that are known to be already initialized *) let non_init_globals = let initialized = snd astate in @@ -109,15 +104,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let globals_trace = SiofTrace.add_sink (SiofTrace.make_access non_init_globals outer_loc) trace in - (Domain.BottomSiofTrace.NonBottom globals_trace, snd astate) + (NonBottom globals_trace, snd astate) let add_params_globals astate pdesc call_loc params = List.map ~f:(fun (e, _) -> get_globals pdesc call_loc e) params |> List.fold ~f:GlobalsAccesses.union ~init:GlobalsAccesses.empty |> add_globals astate (Procdesc.get_loc pdesc) - let at_least_nonbottom = - Domain.join (Domain.BottomSiofTrace.NonBottom SiofTrace.empty, Domain.VarNames.empty) + let at_least_nonbottom = Domain.join (NonBottom SiofTrace.empty, Domain.VarNames.empty) let exec_instr astate {ProcData.pdesc} _ (instr: Sil.instr) = match instr with @@ -135,8 +129,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct then Some initialized_globals else None ) in - Domain.join astate - (Domain.BottomSiofTrace.NonBottom SiofTrace.empty, Domain.VarNames.of_list init) + Domain.join astate (NonBottom SiofTrace.empty, Domain.VarNames.of_list init) | Call (_, Const Cfun callee_pname, _ :: params_without_self, loc, _) when Typ.Procname.is_c_method callee_pname && Typ.Procname.is_constructor callee_pname && Typ.Procname.is_constexpr callee_pname @@ -145,7 +138,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct -> let callsite = CallSite.make callee_pname loc in let callee_astate = match Summary.read_summary pdesc callee_pname with - | Some (Domain.BottomSiofTrace.NonBottom trace, initialized_globals) + | Some (NonBottom trace, initialized_globals) -> let trace_without_initialized_globals = let sinks_with_non_init_globals = SiofTrace.Sinks.filter @@ -156,13 +149,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in SiofTrace.update_sinks trace sinks_with_non_init_globals in - ( Domain.BottomSiofTrace.NonBottom - (SiofTrace.with_callsite trace_without_initialized_globals callsite) + ( NonBottom (SiofTrace.with_callsite trace_without_initialized_globals callsite) , initialized_globals ) - | Some (Domain.BottomSiofTrace.Bottom, _ as astate) + | Some (Bottom, _ as astate) -> astate | None - -> (Domain.BottomSiofTrace.Bottom, Domain.VarNames.empty) + -> (Bottom, Domain.VarNames.empty) in add_params_globals astate pdesc loc params |> Domain.join callee_astate |> (* make sure it's not Bottom: we made a function call so this needs initialization *) @@ -193,7 +185,7 @@ let report_siof summary trace pdesc gname loc = in let trace_of_pname pname = match Summary.read_summary pdesc pname with - | Some (SiofDomain.BottomSiofTrace.NonBottom summary, _) + | Some (NonBottom summary, _) -> summary | _ -> SiofTrace.empty @@ -233,7 +225,7 @@ let report_siof summary trace pdesc gname loc = let siof_check pdesc gname (summary: Specs.summary) = match summary.payload.siof with - | Some (SiofDomain.BottomSiofTrace.NonBottom post, _) + | Some (NonBottom post, _) -> let attrs = Procdesc.get_attributes pdesc in let all_globals = SiofTrace.Sinks.fold @@ -246,12 +238,12 @@ let siof_check pdesc gname (summary: Specs.summary) = in if GlobalsAccesses.exists (is_foreign tu_opt) all_globals then report_siof summary post pdesc gname attrs.ProcAttributes.loc - | Some (SiofDomain.BottomSiofTrace.Bottom, _) | None + | Some (Bottom, _) | None -> () let checker {Callbacks.proc_desc; tenv; summary} : Specs.summary = let proc_data = ProcData.make_default proc_desc tenv in - let initial = (SiofDomain.BottomSiofTrace.Bottom, SiofDomain.VarNames.empty) in + let initial = (Bottom, SiofDomain.VarNames.empty) in let updated_summary = match Analyzer.compute_post proc_data ~initial with | Some post diff --git a/infer/src/checkers/SiofDomain.ml b/infer/src/checkers/SiofDomain.ml index 56e2fe31c..0723982b9 100644 --- a/infer/src/checkers/SiofDomain.ml +++ b/infer/src/checkers/SiofDomain.ml @@ -8,6 +8,7 @@ *) open! IStd +open! AbstractDomain.Types module VarNames = AbstractDomain.FiniteSet (String) module BottomSiofTrace = AbstractDomain.BottomLifted (SiofTrace) include AbstractDomain.Pair (BottomSiofTrace) (VarNames) @@ -15,9 +16,9 @@ include AbstractDomain.Pair (BottomSiofTrace) (VarNames) (** group together procedure-local accesses *) let normalize (trace, initialized as astate) = match trace with - | BottomSiofTrace.Bottom + | Bottom -> astate - | BottomSiofTrace.NonBottom trace + | NonBottom trace -> let elems = SiofTrace.Sinks.elements (SiofTrace.sinks trace) in let direct, indirect = List.partition_tf ~f:SiofTrace.is_intraprocedural_access elems in match direct with @@ -35,4 +36,4 @@ let normalize (trace, initialized as astate) = SiofTrace.make_access kind loc :: indirect |> SiofTrace.Sinks.of_list |> SiofTrace.update_sinks trace in - (BottomSiofTrace.NonBottom trace', initialized) + (NonBottom trace', initialized) diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index 6936fd263..05840bde3 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -8,6 +8,7 @@ *) open! IStd +open! AbstractDomain.Types module F = Format module L = Logging module MF = MarkupFormatter @@ -21,9 +22,9 @@ module Domain = struct let add_call_site annot sink call_site (annot_map, previous_vstate as astate) = match previous_vstate with - | TrackingDomain.Bottom + | Bottom -> astate - | TrackingDomain.NonBottom _ + | NonBottom _ -> let sink_map = try AnnotReachabilityDomain.find annot annot_map with Not_found -> AnnotReachabilityDomain.SinkMap.empty @@ -37,28 +38,24 @@ module Domain = struct if phys_equal sink_map' sink_map then astate else (AnnotReachabilityDomain.add annot sink_map' annot_map, previous_vstate) - let stop_tracking ((annot_map, _): astate) = (annot_map, TrackingDomain.Bottom) + let stop_tracking ((annot_map, _): astate) = (annot_map, Bottom) let add_tracking_var var (annot_map, previous_vstate as astate) = match previous_vstate with - | TrackingDomain.Bottom + | Bottom -> astate - | TrackingDomain.NonBottom vars - -> (annot_map, TrackingDomain.NonBottom (TrackingVar.add var vars)) + | NonBottom vars + -> (annot_map, NonBottom (TrackingVar.add var vars)) let remove_tracking_var var (annot_map, previous_vstate as astate) = match previous_vstate with - | TrackingDomain.Bottom + | Bottom -> astate - | TrackingDomain.NonBottom vars - -> (annot_map, TrackingDomain.NonBottom (TrackingVar.remove var vars)) + | NonBottom vars + -> (annot_map, NonBottom (TrackingVar.remove var vars)) let is_tracked_var var (_, vstate) = - match vstate with - | TrackingDomain.Bottom - -> false - | TrackingDomain.NonBottom vars - -> TrackingVar.mem var vars + match vstate with Bottom -> false | NonBottom vars -> TrackingVar.mem var vars end module Summary = Summary.Make (struct @@ -434,9 +431,7 @@ end module Analyzer = AbstractInterpreter.Make (ProcCfg.Exceptional) (TransferFunctions) let checker ({Callbacks.proc_desc; tenv; summary} as callback) : Specs.summary = - let initial = - (AnnotReachabilityDomain.empty, Domain.TrackingDomain.NonBottom Domain.TrackingVar.empty) - in + let initial = (AnnotReachabilityDomain.empty, NonBottom Domain.TrackingVar.empty) in let proc_data = ProcData.make_default proc_desc tenv in match Analyzer.compute_post proc_data ~initial with | Some (annot_map, _)