From fb69d8aca1d14b2b05fb0340eafa201a11814ddf Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 29 Jun 2021 05:57:49 -0700 Subject: [PATCH] [pulse] use phys_equal on the underlying abstract state instead of the toplevel pair Summary: This is more useful for a future where we use the exceptional CFG but even without it we see some non-trivial changes on OpenSSL (slightly fewer total disjunts): Before: ``` Found 57 issues (console output truncated to 5, see '/home/jul/code/openssl-1.0.2d/infer-out/report.txt' for the full list) Issue Type(ISSUED_TYPE_ID): # Memory Leak(MEMORY_LEAK): 48 Nullptr Dereference(NULLPTR_DEREFERENCE): 6 Uninitialized Value(PULSE_UNINITIALIZED_VALUE): 3 infer --pulse-only --scheduler restart --pulse-model-malloc-pattern 387.55s user 7.20s system 192% cpu 3:24.60 total average #disjuncts: 7.695755 total #disjuncts: 64906 min= 0; p10= 0; p20= 1; p25= 1; p30= 1; p40= 1; p50= 2; p60= 4; p70= 18; p75= 20; p80= 20; p90= 20; p95= 20; p96= 20; p97= 20; p98= 20; p99= 20; max= 20 51253 continue 67 exit 1101 abort 9606 latent abort 2879 latent invalid ``` After: ``` Found 64 issues (console output truncated to 5, see '/home/jul/code/openssl-1.0.2d/infer-out/report.txt' for the full list) Issue Type(ISSUED_TYPE_ID): # Memory Leak(MEMORY_LEAK): 55 Nullptr Dereference(NULLPTR_DEREFERENCE): 6 Uninitialized Value(PULSE_UNINITIALIZED_VALUE): 3 infer --pulse-only --scheduler restart --pulse-model-malloc-pattern 371.63s user 6.62s system 196% cpu 3:12.41 total average #disjuncts: 7.537230 total #disjuncts: 63569 min= 0; p10= 0; p20= 1; p25= 1; p30= 1; p40= 1; p50= 2; p60= 4; p70= 16; p75= 20; p80= 20; p90= 20; p95= 20; p96= 20; p97= 20; p98= 20; p99= 20; max= 20 53763 continue 67 exit 1022 abort 6270 latent abort 2447 latent invalid ``` Reviewed By: ezgicicek Differential Revision: D29230744 fbshipit-source-id: 5c76c275f --- infer/src/absint/AbstractDomain.ml | 22 ++++++++++++++++++---- infer/src/absint/AbstractDomain.mli | 15 ++++++++++++--- infer/src/absint/AbstractInterpreter.ml | 6 +++--- infer/src/absint/TransferFunctions.ml | 2 +- infer/src/absint/TransferFunctions.mli | 2 +- infer/src/pulse/Pulse.ml | 10 +++++----- infer/src/pulse/PulseExecutionDomain.ml | 13 +++++++++++++ infer/src/pulse/PulseExecutionDomain.mli | 2 +- infer/src/pulse/PulsePathContext.ml | 3 +++ infer/src/pulse/PulsePathContext.mli | 2 ++ 10 files changed, 59 insertions(+), 18 deletions(-) diff --git a/infer/src/absint/AbstractDomain.ml b/infer/src/absint/AbstractDomain.ml index ad0e4806a..7dcb924ee 100644 --- a/infer/src/absint/AbstractDomain.ml +++ b/infer/src/absint/AbstractDomain.ml @@ -18,14 +18,22 @@ end open! Types -module type NoJoin = sig +module type Comparable = sig include PrettyPrintable.PrintableType val leq : lhs:t -> rhs:t -> bool end +module type Disjunct = sig + include Comparable + + val equal_fast : t -> t -> bool +end + module type S = sig - include NoJoin + include PrettyPrintable.PrintableType + + val leq : lhs:t -> rhs:t -> bool val join : t -> t -> t @@ -175,7 +183,7 @@ module TopLifted (Domain : S) = struct let pp = TopLiftedUtils.pp ~pp:Domain.pp end -module PairNoJoin (Domain1 : NoJoin) (Domain2 : NoJoin) = struct +module PairBase (Domain1 : Comparable) (Domain2 : Comparable) = struct type t = Domain1.t * Domain2.t let leq ~lhs ~rhs = @@ -186,8 +194,14 @@ module PairNoJoin (Domain1 : NoJoin) (Domain2 : NoJoin) = struct let pp fmt astate = Pp.pair ~fst:Domain1.pp ~snd:Domain2.pp fmt astate end +module PairDisjunct (Domain1 : Disjunct) (Domain2 : Disjunct) = struct + include PairBase (Domain1) (Domain2) + + let equal_fast (x1, x2) (y1, y2) = Domain1.equal_fast x1 y1 && Domain2.equal_fast x2 y2 +end + module Pair (Domain1 : S) (Domain2 : S) = struct - include PairNoJoin (Domain1) (Domain2) + include PairBase (Domain1) (Domain2) let join astate1 astate2 = if phys_equal astate1 astate2 then astate1 diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli index e31a512fd..918459f7a 100644 --- a/infer/src/absint/AbstractDomain.mli +++ b/infer/src/absint/AbstractDomain.mli @@ -19,15 +19,23 @@ end open! Types -module type NoJoin = sig +module type Comparable = sig include PrettyPrintable.PrintableType val leq : lhs:t -> rhs:t -> bool (** the implication relation: [lhs <= rhs] means [lhs |- rhs] *) end +module type Disjunct = sig + include Comparable + + val equal_fast : t -> t -> bool + (** [equal_fast x y] must imply [x <=> y]; it's a good idea for this function to be "fast", e.g. + not depend on the size of its input *) +end + module type S = sig - include NoJoin + include Comparable val join : t -> t -> t @@ -83,7 +91,8 @@ end (** Cartesian product of two domains. *) module Pair (Domain1 : S) (Domain2 : S) : S with type t = Domain1.t * Domain2.t -module PairNoJoin (Domain1 : NoJoin) (Domain2 : NoJoin) : NoJoin with type t = Domain1.t * Domain2.t +module PairDisjunct (Domain1 : Disjunct) (Domain2 : Disjunct) : + Disjunct with type t = Domain1.t * Domain2.t (** Flat abstract domain: Bottom, Top, and non-comparable elements in between *) module Flat (V : PrettyPrintable.PrintableEquatableType) : sig diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index d728f605f..11b899bfe 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -162,7 +162,7 @@ struct let join_up_to ~limit ~into:lhs rhs = - join_up_to_with_leq ~limit (fun ~lhs ~rhs -> phys_equal lhs rhs) ~into:lhs rhs + join_up_to_with_leq ~limit (fun ~lhs ~rhs -> T.Domain.equal_fast lhs rhs) ~into:lhs rhs let join lhs rhs = join_up_to ~limit:disjunct_limit ~into:lhs rhs |> fst @@ -173,7 +173,7 @@ struct match (disj, of_) with | [], _ -> true - | x :: disj', y :: of' when phys_equal x y -> + | x :: disj', y :: of' when T.Domain.equal_fast x y -> is_trivial_subset disj' ~of_:of' | _, _ :: of' -> is_trivial_subset disj ~of_:of' @@ -229,7 +229,7 @@ struct | None -> true | Some {State.pre= previous_pre; _} -> - not (List.mem ~equal:phys_equal previous_pre disjunct) + not (List.mem ~equal:T.Domain.equal_fast previous_pre disjunct) in let current_post_n = match old_state_opt with None -> ([], 0) | Some {State.post; _} -> (post, List.length post) diff --git a/infer/src/absint/TransferFunctions.ml b/infer/src/absint/TransferFunctions.ml index 544d0430e..b87573e3f 100644 --- a/infer/src/absint/TransferFunctions.ml +++ b/infer/src/absint/TransferFunctions.ml @@ -43,7 +43,7 @@ end module type DisjReady = sig module CFG : ProcCfg.S - module Domain : AbstractDomain.NoJoin + module Domain : AbstractDomain.Disjunct type analysis_data diff --git a/infer/src/absint/TransferFunctions.mli b/infer/src/absint/TransferFunctions.mli index 7715b2727..741b23594 100644 --- a/infer/src/absint/TransferFunctions.mli +++ b/infer/src/absint/TransferFunctions.mli @@ -55,7 +55,7 @@ end module type DisjReady = sig module CFG : ProcCfg.S - module Domain : AbstractDomain.NoJoin + module Domain : AbstractDomain.Disjunct type analysis_data diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 566f8ea9d..7029e2343 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -25,7 +25,7 @@ let report_topl_errors proc_desc err_log summary = module PulseTransferFunctions = struct module CFG = ProcCfg.Normal - module Domain = AbstractDomain.PairNoJoin (PathContext) (ExecutionDomain) + module Domain = AbstractDomain.PairDisjunct (ExecutionDomain) (PathContext) type analysis_data = PulseSummary.t InterproceduralAnalysis.t @@ -443,13 +443,13 @@ module PulseTransferFunctions = struct [ContinueProgram astate] ) - let exec_instr (path, astate) analysis_data cfg_node instr : Domain.t list = + let exec_instr (astate, path) analysis_data cfg_node instr : Domain.t list = (* Sometimes instead of stopping on contradictions a false path condition is recorded instead. Prune these early here so they don't spuriously count towards the disjunct limit. *) exec_instr_aux path astate analysis_data cfg_node instr |> List.filter_map ~f:(fun exec_state -> if ExecutionDomain.is_unsat_cheap exec_state then None - else Some (PathContext.post_exec_instr path, exec_state) ) + else Some (exec_state, PathContext.post_exec_instr path) ) let pp_session_name _node fmt = F.pp_print_string fmt "Pulse" @@ -474,11 +474,11 @@ let with_debug_exit_node proc_desc ~f = let checker ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) = AbstractValue.State.reset () ; let initial_astate = ExecutionDomain.mk_initial tenv proc_desc in - let initial = [(PathContext.initial, initial_astate)] in + let initial = [(initial_astate, PathContext.initial)] in match DisjunctiveAnalyzer.compute_post analysis_data ~initial proc_desc with | Some posts -> (* forget path contexts, we don't propagate them across functions *) - let posts = List.map ~f:snd posts in + let posts = List.map ~f:fst posts in with_debug_exit_node proc_desc ~f:(fun () -> let updated_posts = PulseObjectiveCSummary.update_objc_method_posts analysis_data ~initial_astate ~posts diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml index afe83e96a..d6f3f7311 100644 --- a/infer/src/pulse/PulseExecutionDomain.ml +++ b/infer/src/pulse/PulseExecutionDomain.ml @@ -93,3 +93,16 @@ let get_astate : t -> AbductiveDomain.t = function let is_unsat_cheap exec_state = PathCondition.is_unsat_cheap (get_astate exec_state).path_condition type summary = AbductiveDomain.summary base_t [@@deriving compare, equal, yojson_of] + +let equal_fast exec_state1 exec_state2 = + phys_equal exec_state1 exec_state2 + || + match (exec_state1, exec_state2) with + | AbortProgram astate1, AbortProgram astate2 + | ExitProgram astate1, ExitProgram astate2 + | ISLLatentMemoryError astate1, ISLLatentMemoryError astate2 -> + phys_equal astate1 astate2 + | ContinueProgram astate1, ContinueProgram astate2 -> + phys_equal astate1 astate2 + | _ -> + false diff --git a/infer/src/pulse/PulseExecutionDomain.mli b/infer/src/pulse/PulseExecutionDomain.mli index 2a721ec32..9c65f584b 100644 --- a/infer/src/pulse/PulseExecutionDomain.mli +++ b/infer/src/pulse/PulseExecutionDomain.mli @@ -31,7 +31,7 @@ type 'abductive_domain_t base_t = type t = AbductiveDomain.t base_t -include AbstractDomain.NoJoin with type t := t +include AbstractDomain.Disjunct with type t := t val continue : AbductiveDomain.t -> t diff --git a/infer/src/pulse/PulsePathContext.ml b/infer/src/pulse/PulsePathContext.ml index e201731a8..09e2072f1 100644 --- a/infer/src/pulse/PulsePathContext.ml +++ b/infer/src/pulse/PulsePathContext.ml @@ -17,6 +17,9 @@ type t = {timestamp: timestamp} (** path contexts is metadata that do not contribute to the semantics *) let leq ~lhs:_ ~rhs:_ = true +(** see [leq] *) +let equal_fast _ _ = true + let pp fmt ({timestamp}[@warning "+9"]) = F.fprintf fmt "timestamp= %d" timestamp let initial = {timestamp= 0} diff --git a/infer/src/pulse/PulsePathContext.mli b/infer/src/pulse/PulsePathContext.mli index 9f8f850cf..0e68ed204 100644 --- a/infer/src/pulse/PulsePathContext.mli +++ b/infer/src/pulse/PulsePathContext.mli @@ -16,6 +16,8 @@ type t = {timestamp: timestamp (** step number *)} val leq : lhs:t -> rhs:t -> bool +val equal_fast : t -> t -> bool + val initial : t val post_exec_instr : t -> t