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 ;