From 50feb5481cfc887e09ff18b98c27f3b18a6c0f07 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 20 Apr 2020 11:00:14 -0700 Subject: [PATCH] [pudge] only ask unsat when reporting Summary: Computing sledge's equality relation and normalising terms is costly. We can avoid doing that most of the time by keeping the sledge path condition lazily evaluated and only forcing it down to a value at two critical points in the analysis: 1. Summary creation, to avoid storing unsatisfiable pre/posts that will have to be needlessly executed by callers. This also saves us from having to serialise the closures involved in the uncomputed form of lazy values inside the pulse summaries. 2. Before reporting errors we check in the state is in fact satisfiable. If not we just prune it away at that point. This yields ~4x speedup on some targets. Reviewed By: ezgicicek Differential Revision: D21129759 fbshipit-source-id: a75fdd3bc --- infer/src/pulse/Pulse.ml | 6 +- infer/src/pulse/PulseAbductiveDomain.ml | 2 - infer/src/pulse/PulseAbductiveDomain.mli | 2 - infer/src/pulse/PulseArithmetic.ml | 85 ++++++++++++------------ infer/src/pulse/PulseArithmetic.mli | 5 +- infer/src/pulse/PulseExecutionDomain.ml | 10 +-- infer/src/pulse/PulseExecutionDomain.mli | 6 +- infer/src/pulse/PulseInterproc.ml | 10 +-- infer/src/pulse/PulseOperations.mli | 2 +- infer/src/pulse/PulseSummary.ml | 2 +- 10 files changed, 65 insertions(+), 65 deletions(-) diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 01ffc0a95..81a1d4c1e 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -22,8 +22,10 @@ let check_error_transform summary ~f = function | Ok astate -> f astate | Error (diagnostic, astate) -> - report summary diagnostic ; - [ExecutionDomain.AbortProgram astate] + if PulseArithmetic.is_unsat astate then [] + else ( + report summary diagnostic ; + [ExecutionDomain.AbortProgram astate] ) let check_error_continue summary result = diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 8abf3f976..db801840e 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -93,8 +93,6 @@ let pp f {post; pre; path_condition; skipped_calls} = PostDomain.pp post PreDomain.pp pre SkippedCalls.pp skipped_calls -let get_path_condition {path_condition} = path_condition - let set_path_condition path_condition astate = {astate with path_condition} let leq ~lhs ~rhs = diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 9764331d0..3ab7bac8b 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -154,8 +154,6 @@ val add_skipped_call : Procname.t -> Trace.t -> t -> t val add_skipped_calls : SkippedCalls.t -> t -> t -val get_path_condition : t -> PathCondition.t - val set_path_condition : PathCondition.t -> t -> t val of_post : Procdesc.t -> t -> t diff --git a/infer/src/pulse/PulseArithmetic.ml b/infer/src/pulse/PulseArithmetic.ml index eae5376df..b2b65dc7c 100644 --- a/infer/src/pulse/PulseArithmetic.ml +++ b/infer/src/pulse/PulseArithmetic.ml @@ -6,19 +6,19 @@ *) open! IStd -module L = Logging open PulseBasicInterface -open PulseDomainInterface +module AbductiveDomain = PulseAbductiveDomain +module AddressAttributes = AbductiveDomain.AddressAttributes (** {2 Building arithmetic constraints} *) let and_eq_terms t1 t2 astate = - let phi = PathCondition.and_eq t1 t2 (AbductiveDomain.get_path_condition astate) in + let phi = PathCondition.and_eq t1 t2 astate.AbductiveDomain.path_condition in AbductiveDomain.set_path_condition phi astate let and_term t astate = - let phi = PathCondition.and_term t (AbductiveDomain.get_path_condition astate) in + let phi = PathCondition.and_term t astate.AbductiveDomain.path_condition in AbductiveDomain.set_path_condition phi astate @@ -197,49 +197,44 @@ let prune_binop ~is_then_branch if_kind location ~negated bop lhs_op rhs_op asta let value_rhs_opt, arith_rhs_opt, bo_itv_rhs, path_cond_rhs = eval_operand location astate rhs_op in - let astate, path_condition = + let astate = let path_condition = let t_positive = PathCondition.Term.of_binop bop path_cond_lhs path_cond_rhs in let t = if negated then PathCondition.Term.not_ t_positive else t_positive in - AbductiveDomain.get_path_condition astate |> PathCondition.and_term t + PathCondition.and_term t astate.AbductiveDomain.path_condition in - let astate = AbductiveDomain.set_path_condition path_condition astate in - (astate, path_condition) + AbductiveDomain.set_path_condition path_condition astate in - if PathCondition.is_unsat path_condition then ( - L.d_printfln "Contradiction detected in path condition" ; - (astate, false) ) - else - match - CItv.abduce_binop_is_true ~negated bop (Option.map ~f:fst arith_lhs_opt) - (Option.map ~f:fst arith_rhs_opt) - with - | Unsatisfiable -> - (astate, false) - | Satisfiable (abduced_lhs, abduced_rhs) -> - let event = ValueHistory.Conditional {is_then_branch; if_kind; location} in - let astate = - record_abduced event location value_lhs_opt arith_lhs_opt abduced_lhs astate - |> record_abduced event location value_rhs_opt arith_rhs_opt abduced_rhs - in - let satisfiable = - match Itv.ItvPure.arith_binop bop bo_itv_lhs bo_itv_rhs |> Itv.ItvPure.to_boolean with - | False -> - negated - | True -> - not negated - | Top -> - true - | Bottom -> - false - in - let astate, satisfiable = + match + CItv.abduce_binop_is_true ~negated bop (Option.map ~f:fst arith_lhs_opt) + (Option.map ~f:fst arith_rhs_opt) + with + | Unsatisfiable -> + (astate, false) + | Satisfiable (abduced_lhs, abduced_rhs) -> + let event = ValueHistory.Conditional {is_then_branch; if_kind; location} in + let astate = + record_abduced event location value_lhs_opt arith_lhs_opt abduced_lhs astate + |> record_abduced event location value_rhs_opt arith_rhs_opt abduced_rhs + in + let satisfiable = + match Itv.ItvPure.arith_binop bop bo_itv_lhs bo_itv_rhs |> Itv.ItvPure.to_boolean with + | False -> + negated + | True -> + not negated + | Top -> + true + | Bottom -> + false + in + let astate, satisfiable = + bind_satisfiable ~satisfiable astate ~f:(fun astate -> + prune_with_bop ~negated value_lhs_opt bo_itv_lhs bop bo_itv_rhs astate ) + in + Option.value_map (Binop.symmetric bop) ~default:(astate, satisfiable) ~f:(fun bop' -> bind_satisfiable ~satisfiable astate ~f:(fun astate -> - prune_with_bop ~negated value_lhs_opt bo_itv_lhs bop bo_itv_rhs astate ) - in - Option.value_map (Binop.symmetric bop) ~default:(astate, satisfiable) ~f:(fun bop' -> - bind_satisfiable ~satisfiable astate ~f:(fun astate -> - prune_with_bop ~negated value_rhs_opt bo_itv_rhs bop' bo_itv_lhs astate ) ) + prune_with_bop ~negated value_rhs_opt bo_itv_rhs bop' bo_itv_lhs astate ) ) (** {2 Queries} *) @@ -247,6 +242,12 @@ let prune_binop ~is_then_branch if_kind location ~negated bop lhs_op rhs_op asta let is_known_zero astate v = ( AddressAttributes.get_citv v astate |> function Some (arith, _) -> CItv.is_equal_to_zero arith | None -> false ) - || (let phi = AbductiveDomain.get_path_condition astate in + || (let phi = astate.AbductiveDomain.path_condition in PathCondition.is_known_zero (PathCondition.Term.of_absval v) phi ) || Itv.ItvPure.is_zero (AddressAttributes.get_bo_itv v astate) + + +let is_unsat astate = + (* note: contradictions are detected eagerly for all domains except path conditions, so just + evaluate that one *) + PathCondition.is_unsat astate.AbductiveDomain.path_condition diff --git a/infer/src/pulse/PulseArithmetic.mli b/infer/src/pulse/PulseArithmetic.mli index 8f3e8e693..02f140ca3 100644 --- a/infer/src/pulse/PulseArithmetic.mli +++ b/infer/src/pulse/PulseArithmetic.mli @@ -7,7 +7,7 @@ open! IStd open PulseBasicInterface -open PulseDomainInterface +module AbductiveDomain = PulseAbductiveDomain (** {2 Building arithmetic constraints} *) @@ -56,3 +56,6 @@ val prune_binop : val is_known_zero : AbductiveDomain.t -> AbstractValue.t -> bool (** [is_known_zero astate t] returns [true] if [astate |- t = 0], [false] if we don't know for sure *) + +val is_unsat : AbductiveDomain.t -> bool +(** returns whether the state contains a contradiction *) diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml index 0ad9e6547..68ecbc44c 100644 --- a/infer/src/pulse/PulseExecutionDomain.ml +++ b/infer/src/pulse/PulseExecutionDomain.ml @@ -9,13 +9,11 @@ open! IStd module F = Format module AbductiveDomain = PulseAbductiveDomain -type exec_state = +type t = | AbortProgram of AbductiveDomain.t | ContinueProgram of AbductiveDomain.t | ExitProgram of AbductiveDomain.t -type t = exec_state - let continue astate = ContinueProgram astate let mk_initial pdesc = ContinueProgram (AbductiveDomain.mk_initial pdesc) @@ -49,4 +47,8 @@ let map ~f exec_state = ExitProgram (f astate) -let of_post pdesc = map ~f:(AbductiveDomain.of_post pdesc) +let of_posts pdesc posts = + List.filter_map posts ~f:(fun exec_state -> + let (AbortProgram astate | ContinueProgram astate | ExitProgram astate) = exec_state in + if PulseArithmetic.is_unsat astate then None + else Some (map exec_state ~f:(AbductiveDomain.of_post pdesc)) ) diff --git a/infer/src/pulse/PulseExecutionDomain.mli b/infer/src/pulse/PulseExecutionDomain.mli index 0d7e38518..446a9210d 100644 --- a/infer/src/pulse/PulseExecutionDomain.mli +++ b/infer/src/pulse/PulseExecutionDomain.mli @@ -6,17 +6,17 @@ *) open! IStd -type exec_state = +type t = | AbortProgram of PulseAbductiveDomain.t (** represents the state at the program point that caused an error *) | ContinueProgram of PulseAbductiveDomain.t (** represents the state at the program point *) | ExitProgram of PulseAbductiveDomain.t (** represents the state originating at exit/divergence. *) -include AbstractDomain.NoJoin with type t = exec_state +include AbstractDomain.NoJoin with type t := t val continue : PulseAbductiveDomain.t -> t -val of_post : Procdesc.t -> t -> t +val of_posts : Procdesc.t -> t list -> t list val mk_initial : Procdesc.t -> t diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index e26723f98..88802d5c7 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -73,7 +73,6 @@ type contradiction = state *) | FormalActualLength of {formals: Var.t list; actuals: ((AbstractValue.t * ValueHistory.t) * Typ.t) list} - | UnsatPathCondition of call_state let pp_contradiction fmt = function | Aliasing {addr_caller; addr_callee; addr_callee'; call_state} -> @@ -95,8 +94,6 @@ let pp_contradiction fmt = function | FormalActualLength {formals; actuals} -> F.fprintf fmt "formals have length %d but actuals have length %d" (List.length formals) (List.length actuals) - | UnsatPathCondition call_state -> - F.fprintf fmt "UNSAT %a" pp_call_state call_state exception Contradiction of contradiction @@ -316,10 +313,9 @@ let conjoin_callee_arith pre_post call_state = in let path_condition = PathCondition.and_ call_state.astate.path_condition callee_path_cond in let astate = AbductiveDomain.set_path_condition path_condition call_state.astate in - let call_state = {call_state with astate; subst} in - if PathCondition.is_unsat path_condition then - raise (Contradiction (UnsatPathCondition call_state)) - else call_state + (* Don't trigger the computation of [path_condition] by asking for satisfiability here. Instead, + (un-)satisfiability is computed lazily when we discover issues. *) + {call_state with astate; subst} (* shadowed to take config into account *) diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index e6ce46abe..ec9f6f225 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -13,7 +13,7 @@ type t = AbductiveDomain.t type 'a access_result = ('a, Diagnostic.t * t) result -val ok_continue : t -> (ExecutionDomain.exec_state list, 'a) result +val ok_continue : t -> (ExecutionDomain.t list, 'a) result module Closures : sig val check_captured_addresses : Location.t -> AbstractValue.t -> t -> (t, Diagnostic.t * t) result diff --git a/infer/src/pulse/PulseSummary.ml b/infer/src/pulse/PulseSummary.ml index 8ee479ae5..ee933d5c2 100644 --- a/infer/src/pulse/PulseSummary.ml +++ b/infer/src/pulse/PulseSummary.ml @@ -11,7 +11,7 @@ open PulseDomainInterface type t = ExecutionDomain.t list -let of_posts pdesc posts = List.map posts ~f:(ExecutionDomain.of_post pdesc) +let of_posts pdesc posts = ExecutionDomain.of_posts pdesc posts let pp fmt summary = F.open_vbox 0 ;