From 5423bb1699971d50db43ad5b9f52759efc59133e Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 4 Dec 2020 07:30:00 -0800 Subject: [PATCH] [pulse] make sure we checked satisfiability on summaries Summary: Made `AbductiveDomain.summary_of_post` return a Sat/Unsat to make sure callers filter unsat summaries. Also made `ExitProgram` take a summary instead of a non-normalized abstract state, which was wrong (mostly could litter the disjuncts with infeasible paths). Reviewed By: skcho Differential Revision: D25277565 fbshipit-source-id: 72dacb944 --- infer/src/checkers/impurity.ml | 2 +- infer/src/pulse/PulseAbductiveDomain.ml | 29 +++++++++----- infer/src/pulse/PulseAbductiveDomain.mli | 2 +- infer/src/pulse/PulseArithmetic.ml | 8 ---- infer/src/pulse/PulseArithmetic.mli | 2 - infer/src/pulse/PulseExecutionDomain.ml | 48 +++++++++--------------- infer/src/pulse/PulseExecutionDomain.mli | 3 +- infer/src/pulse/PulseModels.ml | 7 +++- infer/src/pulse/PulseOperations.ml | 38 +++++++++---------- infer/src/pulse/PulsePathCondition.ml | 20 ++++++---- infer/src/pulse/PulsePathCondition.mli | 4 +- infer/src/pulse/PulseReport.ml | 21 +++++------ 12 files changed, 91 insertions(+), 93 deletions(-) diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index cc0276c79..da3b06df5 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -158,7 +158,7 @@ let extract_impurity tenv pname formals (exec_state : ExecutionDomain.t) : Impur let astate, exited = match exec_state with | ExitProgram astate -> - (astate, true) + ((astate :> AbductiveDomain.t), true) | ContinueProgram astate -> (astate, false) | AbortProgram astate | LatentAbortProgram {astate} -> diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 6adac2a81..cb86c2c5c 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -456,31 +456,34 @@ let is_allocated {post; pre} v = || is_stack_allocated (post :> BaseDomain.t) v -let incorporate_new_eqs astate (phi, new_eqs) = - List.fold_until new_eqs ~init:phi ~finish:Fn.id ~f:(fun phi (new_eq : PulseFormula.new_eq) -> +let incorporate_new_eqs astate new_eqs = + List.fold_until new_eqs ~init:() + ~finish:(fun () -> Sat ()) + ~f:(fun () (new_eq : PulseFormula.new_eq) -> match new_eq with | EqZero v when is_allocated astate v -> L.d_printfln "CONTRADICTION: %a = 0 but is allocated" AbstractValue.pp v ; - Stop PathCondition.false_ + Stop Unsat | Equal (v1, v2) when (not (AbstractValue.equal v1 v2)) && is_allocated astate v1 && is_allocated astate v2 -> L.d_printfln "CONTRADICTION: %a = %a but both are separately allocated" AbstractValue.pp v1 AbstractValue.pp v2 ; - Stop PathCondition.false_ + Stop Unsat | _ -> - Continue phi ) + Continue () ) let summary_of_post pdesc astate = + let open SatUnsat.Import in let astate = filter_for_summary astate in let astate, live_addresses, _ = discard_unreachable astate in + let* path_condition, new_eqs = + PathCondition.simplify ~keep:live_addresses astate.path_condition + in + let+ () = incorporate_new_eqs astate new_eqs in let astate = - { astate with - path_condition= - PathCondition.simplify ~keep:live_addresses astate.path_condition - |> incorporate_new_eqs astate - ; topl= PulseTopl.simplify ~keep:live_addresses astate.topl } + {astate with path_condition; topl= PulseTopl.simplify ~keep:live_addresses astate.topl} in invalidate_locals pdesc astate @@ -489,6 +492,12 @@ let get_pre {pre} = (pre :> BaseDomain.t) let get_post {post} = (post :> BaseDomain.t) +(* re-exported for mli *) +let incorporate_new_eqs astate (phi, new_eqs) = + if PathCondition.is_unsat_cheap phi then phi + else match incorporate_new_eqs astate new_eqs with Unsat -> PathCondition.false_ | Sat () -> phi + + module Topl = struct let small_step loc event astate = {astate with topl= PulseTopl.small_step loc astate.path_condition event astate.topl} diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index bf9150bf2..a2ff20e3d 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -164,7 +164,7 @@ val set_path_condition : PathCondition.t -> t -> t (** private type to make sure {!summary_of_post} is always called when creating summaries *) type summary = private t [@@deriving yojson_of] -val summary_of_post : Procdesc.t -> t -> summary +val summary_of_post : Procdesc.t -> t -> summary SatUnsat.t (** trim the state down to just the procedure's interface (formals and globals), and simplify and normalize the state *) diff --git a/infer/src/pulse/PulseArithmetic.ml b/infer/src/pulse/PulseArithmetic.ml index e2557d5c3..eb78628de 100644 --- a/infer/src/pulse/PulseArithmetic.ml +++ b/infer/src/pulse/PulseArithmetic.ml @@ -52,13 +52,5 @@ let is_known_zero astate v = PathCondition.is_known_zero astate.AbductiveDomain. let is_unsat_cheap astate = PathCondition.is_unsat_cheap astate.AbductiveDomain.path_condition -let is_unsat_expensive astate = - let phi', is_unsat, new_eqs = - PathCondition.is_unsat_expensive astate.AbductiveDomain.path_condition - in - let phi' = AbductiveDomain.incorporate_new_eqs astate (phi', new_eqs) in - (AbductiveDomain.set_path_condition phi' astate, is_unsat) - - let has_no_assumptions astate = PathCondition.has_no_assumptions astate.AbductiveDomain.path_condition diff --git a/infer/src/pulse/PulseArithmetic.mli b/infer/src/pulse/PulseArithmetic.mli index 1c986714f..807849c59 100644 --- a/infer/src/pulse/PulseArithmetic.mli +++ b/infer/src/pulse/PulseArithmetic.mli @@ -34,6 +34,4 @@ val is_known_zero : AbductiveDomain.t -> AbstractValue.t -> bool val is_unsat_cheap : AbductiveDomain.t -> bool -val is_unsat_expensive : AbductiveDomain.t -> AbductiveDomain.t * bool - val has_no_assumptions : AbductiveDomain.t -> bool diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml index 5dd022ac9..8b21d4ce6 100644 --- a/infer/src/pulse/PulseExecutionDomain.ml +++ b/infer/src/pulse/PulseExecutionDomain.ml @@ -18,7 +18,7 @@ module LatentIssue = PulseLatentIssue normalized them and don't need to normalize them again. *) type 'abductive_domain_t base_t = | ContinueProgram of 'abductive_domain_t - | ExitProgram of 'abductive_domain_t + | ExitProgram of AbductiveDomain.summary | AbortProgram of AbductiveDomain.summary | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t} [@@deriving yojson_of] @@ -31,10 +31,10 @@ let mk_initial pdesc = ContinueProgram (AbductiveDomain.mk_initial pdesc) let leq ~lhs ~rhs = match (lhs, rhs) with - | AbortProgram astate1, AbortProgram astate2 -> - AbductiveDomain.leq ~lhs:(astate1 :> AbductiveDomain.t) ~rhs:(astate2 :> AbductiveDomain.t) - | ContinueProgram astate1, ContinueProgram astate2 | ExitProgram astate1, ExitProgram astate2 -> + | AbortProgram astate1, AbortProgram astate2 | ExitProgram astate1, ExitProgram astate2 -> AbductiveDomain.leq ~lhs:(astate1 :> AbductiveDomain.t) ~rhs:(astate2 :> AbductiveDomain.t) + | ContinueProgram astate1, ContinueProgram astate2 -> + AbductiveDomain.leq ~lhs:astate1 ~rhs:astate2 | ( LatentAbortProgram {astate= astate1; latent_issue= issue1} , LatentAbortProgram {astate= astate2; latent_issue= issue2} ) -> LatentIssue.equal issue1 issue2 @@ -59,34 +59,22 @@ let pp fmt = function (astate :> AbductiveDomain.t) -let map ~f exec_state = - match exec_state with - | ContinueProgram astate -> - ContinueProgram (f astate) - | ExitProgram astate -> - ExitProgram (f astate) - | AbortProgram astate -> - AbortProgram astate - | LatentAbortProgram {astate; latent_issue} -> - LatentAbortProgram {astate; latent_issue} - - type summary = AbductiveDomain.summary base_t [@@deriving yojson_of] let summary_of_posts pdesc posts = List.filter_mapi posts ~f:(fun i exec_state -> - let astate = - match exec_state with - | AbortProgram astate | LatentAbortProgram {astate} -> - (astate :> AbductiveDomain.t) - | ContinueProgram astate | ExitProgram astate -> - astate - in L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ; - let astate, is_unsat = PulseArithmetic.is_unsat_expensive astate in - if is_unsat then None - else - Some - (map exec_state ~f:(fun _astate -> - (* prefer [astate] since it is an equivalent state that has been normalized *) - AbductiveDomain.summary_of_post pdesc astate )) ) + match exec_state with + | ContinueProgram astate -> ( + match AbductiveDomain.summary_of_post pdesc astate with + | Unsat -> + None + | Sat astate -> + Some (ContinueProgram astate) ) + (* already a summary but need to reconstruct the variants to make the type system happy *) + | AbortProgram astate -> + Some (AbortProgram astate) + | ExitProgram astate -> + Some (ExitProgram astate) + | LatentAbortProgram {astate; latent_issue} -> + Some (LatentAbortProgram {astate; latent_issue}) ) diff --git a/infer/src/pulse/PulseExecutionDomain.mli b/infer/src/pulse/PulseExecutionDomain.mli index f5540628f..df2a4c30b 100644 --- a/infer/src/pulse/PulseExecutionDomain.mli +++ b/infer/src/pulse/PulseExecutionDomain.mli @@ -11,7 +11,8 @@ module LatentIssue = PulseLatentIssue type 'abductive_domain_t base_t = | ContinueProgram of 'abductive_domain_t (** represents the state at the program point *) - | ExitProgram of 'abductive_domain_t (** represents the state originating at exit/divergence. *) + | ExitProgram of AbductiveDomain.summary + (** represents the state originating at exit/divergence. *) | AbortProgram of AbductiveDomain.summary (** represents the state at the program point that caused an error *) | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t} diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 520119308..9fc895093 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -48,7 +48,12 @@ module Misc = struct let early_exit : model = - fun _ ~callee_procname:_ _ ~ret:_ astate -> Ok [ExecutionDomain.ExitProgram astate] + fun {proc_desc} ~callee_procname:_ _ ~ret:_ astate -> + match AbductiveDomain.summary_of_post proc_desc astate with + | Unsat -> + Ok [] + | Sat astate -> + Ok [ExecutionDomain.ExitProgram astate] let return_int : Int64.t -> model = diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 3b92140de..e96bb8fe3 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -468,31 +468,31 @@ let apply_callee ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret f post in let open ExecutionDomain in + let open SatUnsat.Import in match callee_exec_state with - | AbortProgram astate -> - map_call_result - (astate :> AbductiveDomain.t) - ~f:(fun astate -> - let astate_summary = AbductiveDomain.summary_of_post caller_proc_desc astate in - Sat (Ok (AbortProgram astate_summary)) ) | ContinueProgram astate -> map_call_result astate ~f:(fun astate -> Sat (Ok (ContinueProgram astate))) - | ExitProgram astate -> - map_call_result astate ~f:(fun astate -> Sat (Ok (ExitProgram astate))) - | LatentAbortProgram {astate; latent_issue} -> + | AbortProgram astate | ExitProgram astate | LatentAbortProgram {astate} -> map_call_result (astate :> AbductiveDomain.t) ~f:(fun astate -> - let astate_summary = AbductiveDomain.summary_of_post caller_proc_desc astate in - if PulseArithmetic.is_unsat_cheap (astate_summary :> AbductiveDomain.t) then Unsat - else - let latent_issue = - LatentIssue.add_call (CallEvent.Call callee_pname, call_loc) latent_issue - in - Sat - ( if LatentIssue.should_report astate_summary then - Error (LatentIssue.to_diagnostic latent_issue, (astate_summary :> AbductiveDomain.t)) - else Ok (LatentAbortProgram {astate= astate_summary; latent_issue}) ) ) + let+ astate_summary = AbductiveDomain.summary_of_post caller_proc_desc astate in + match callee_exec_state with + | ContinueProgram _ -> + assert false + | AbortProgram _ -> + Ok (AbortProgram astate_summary) + | ExitProgram _ -> + Ok (ExitProgram astate_summary) + | LatentAbortProgram {latent_issue} -> + let latent_issue = + LatentIssue.add_call (CallEvent.Call callee_pname, call_loc) latent_issue + in + if LatentIssue.should_report astate_summary then + Error + ( LatentIssue.to_diagnostic latent_issue + , (astate_summary : AbductiveDomain.summary :> AbductiveDomain.t) ) + else Ok (LatentAbortProgram {astate= astate_summary; latent_issue}) ) let get_captured_actuals location ~captured_vars ~actual_closure astate = diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml index e881f8d4e..0e5923c66 100644 --- a/infer/src/pulse/PulsePathCondition.ml +++ b/infer/src/pulse/PulsePathCondition.ml @@ -13,6 +13,7 @@ module CItv = PulseCItv module Formula = PulseFormula module SatUnsat = PulseSatUnsat module ValueHistory = PulseValueHistory +open SatUnsat.Types module BoItvs = struct include PrettyPrintable.MakePPMonoMap (AbstractValue) (Itv.ItvPure) @@ -100,14 +101,17 @@ let and_eq_vars v1 v2 phi = let simplify ~keep phi = - let+ {is_unsat; bo_itvs; citvs; formula} = phi in - let+| formula, new_eqs = Formula.simplify ~keep formula in - let is_in_keep v _ = AbstractValue.Set.mem v keep in - ( { is_unsat - ; bo_itvs= BoItvs.filter is_in_keep bo_itvs - ; citvs= CItvs.filter is_in_keep citvs - ; formula } - , new_eqs ) + let result = + let+ {is_unsat; bo_itvs; citvs; formula} = phi in + let+| formula, new_eqs = Formula.simplify ~keep formula in + let is_in_keep v _ = AbstractValue.Set.mem v keep in + ( { is_unsat + ; bo_itvs= BoItvs.filter is_in_keep bo_itvs + ; citvs= CItvs.filter is_in_keep citvs + ; formula } + , new_eqs ) + in + if (fst result).is_unsat then Unsat else Sat result let subst_find_or_new subst addr_callee = diff --git a/infer/src/pulse/PulsePathCondition.mli b/infer/src/pulse/PulsePathCondition.mli index 2159375df..ea1ea8702 100644 --- a/infer/src/pulse/PulsePathCondition.mli +++ b/infer/src/pulse/PulsePathCondition.mli @@ -8,6 +8,7 @@ open! IStd module F = Format module AbstractValue = PulseAbstractValue +module SatUnsat = PulseSatUnsat module ValueHistory = PulseValueHistory type t [@@deriving yojson_of] @@ -33,7 +34,7 @@ val and_eq_int : AbstractValue.t -> IntLit.t -> t -> t * new_eqs val and_eq_vars : AbstractValue.t -> AbstractValue.t -> t -> t * new_eqs -val simplify : keep:AbstractValue.Set.t -> t -> t * new_eqs +val simplify : keep:AbstractValue.Set.t -> t -> (t * new_eqs) SatUnsat.t (** [simplify ~keep phi] attempts to get rid of as many variables in [fv phi] but not in [keep] as possible *) @@ -65,6 +66,7 @@ val is_unsat_cheap : t -> bool (** whether the state contains a contradiction, call this as often as you want *) val is_unsat_expensive : t -> t * bool * new_eqs + [@@warning "-32"] (** whether the state contains a contradiction, only call this when you absolutely have to *) val as_int : t -> AbstractValue.t -> int option diff --git a/infer/src/pulse/PulseReport.ml b/infer/src/pulse/PulseReport.ml index 3f972aed4..41110b5be 100644 --- a/infer/src/pulse/PulseReport.ml +++ b/infer/src/pulse/PulseReport.ml @@ -32,15 +32,14 @@ let report_latent_issue proc_desc err_log latent_issue = let report_error proc_desc err_log access_result = + let open SatUnsat.Import in Result.map_error access_result ~f:(fun (diagnostic, astate) -> - let astate_summary = AbductiveDomain.summary_of_post proc_desc astate in - if PulseArithmetic.is_unsat_cheap (astate_summary :> AbductiveDomain.t) then Unsat - else - match LatentIssue.should_report_diagnostic astate_summary diagnostic with - | `ReportNow -> - report proc_desc err_log diagnostic ; - Sat (ExecutionDomain.AbortProgram astate_summary) - | `DelayReport latent_issue -> - if Config.pulse_report_latent_issues then - report_latent_issue proc_desc err_log latent_issue ; - Sat (ExecutionDomain.LatentAbortProgram {astate= astate_summary; latent_issue}) ) + let+ astate_summary = AbductiveDomain.summary_of_post proc_desc astate in + match LatentIssue.should_report_diagnostic astate_summary diagnostic with + | `ReportNow -> + report proc_desc err_log diagnostic ; + ExecutionDomain.AbortProgram astate_summary + | `DelayReport latent_issue -> + if Config.pulse_report_latent_issues then + report_latent_issue proc_desc err_log latent_issue ; + ExecutionDomain.LatentAbortProgram {astate= astate_summary; latent_issue} )