From a64f311ea8fdcc99314ce54c29297ca27952c989 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 13 Aug 2020 03:11:41 -0700 Subject: [PATCH] [formula] remember results of normalization Summary: Normalization is potentially expensive and its result should be remembered if the formula keeps being used. In the future we might use this to make normalization more incremental. Also rename PathCondition.satisfiable -> is_unsat to match PulseFormula.is_unsat. Reviewed By: skcho Differential Revision: D22728264 fbshipit-source-id: 7759b33ac --- infer/src/pulse/Pulse.ml | 3 +- infer/src/pulse/PulseArithmetic.ml | 3 +- infer/src/pulse/PulseArithmetic.mli | 2 +- infer/src/pulse/PulseExecutionDomain.ml | 9 +- infer/src/pulse/PulsePathCondition.ml | 104 +++++++++++++----------- infer/src/pulse/PulsePathCondition.mli | 2 +- 6 files changed, 68 insertions(+), 55 deletions(-) diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index dc207ecee..578361bad 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -22,7 +22,8 @@ let check_error_transform analysis_data ~f = function | Ok astate -> f astate | Error (diagnostic, astate) -> - if PulseArithmetic.is_unsat_expensive astate then [] + let astate, is_unsat = PulseArithmetic.is_unsat_expensive astate in + if is_unsat then [] else ( report analysis_data diagnostic ; [ExecutionDomain.AbortProgram astate] ) diff --git a/infer/src/pulse/PulseArithmetic.ml b/infer/src/pulse/PulseArithmetic.ml index 136611d2d..2f6dc24a3 100644 --- a/infer/src/pulse/PulseArithmetic.ml +++ b/infer/src/pulse/PulseArithmetic.ml @@ -50,4 +50,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 = - PathCondition.is_unsat_expensive astate.AbductiveDomain.path_condition + let phi', is_unsat = PathCondition.is_unsat_expensive astate.AbductiveDomain.path_condition in + (AbductiveDomain.set_path_condition phi' astate, is_unsat) diff --git a/infer/src/pulse/PulseArithmetic.mli b/infer/src/pulse/PulseArithmetic.mli index 138822587..0d5e440ac 100644 --- a/infer/src/pulse/PulseArithmetic.mli +++ b/infer/src/pulse/PulseArithmetic.mli @@ -34,4 +34,4 @@ val is_known_zero : AbductiveDomain.t -> AbstractValue.t -> bool val is_unsat_cheap : AbductiveDomain.t -> bool -val is_unsat_expensive : AbductiveDomain.t -> bool +val is_unsat_expensive : AbductiveDomain.t -> AbductiveDomain.t * bool diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml index 459e44efd..2b8428d7d 100644 --- a/infer/src/pulse/PulseExecutionDomain.ml +++ b/infer/src/pulse/PulseExecutionDomain.ml @@ -52,5 +52,10 @@ let of_posts pdesc posts = List.filter_mapi posts ~f:(fun i exec_state -> let (AbortProgram astate | ContinueProgram astate | ExitProgram astate) = exec_state in L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ; - if PulseArithmetic.is_unsat_expensive astate then None - else Some (map exec_state ~f:(AbductiveDomain.of_post pdesc)) ) + 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.of_post pdesc astate )) ) diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml index 40b0262d4..608e8a886 100644 --- a/infer/src/pulse/PulsePathCondition.ml +++ b/infer/src/pulse/PulsePathCondition.ml @@ -29,59 +29,60 @@ module CItvs = PrettyPrintable.MakePPMonoMap (AbstractValue) (CItv) (** A mash-up of several arithmetic domains. At the moment they are independent, i.e. we don't use facts deduced by one domain to inform another. *) type t = - { satisfiable: bool - (** If [true] then [formula] could still be unsatisfiable (asking that question is + { is_unsat: bool + (** If [false] then [formula] could still be unsatisfiable (asking that question is expensive). - If [false] then the other components of the record can be arbitrary. *) + If [true] then the other components of the record can be arbitrary. *) ; bo_itvs: BoItvs.t ; citvs: CItvs.t ; formula: Formula.t } -let pp fmt {satisfiable; bo_itvs; citvs; formula} = - F.fprintf fmt "@[sat:%b,@;bo: @[%a@],@;citv: @[%a@],@;formula: @[%a@]@]" satisfiable BoItvs.pp +let pp fmt {is_unsat; bo_itvs; citvs; formula} = + F.fprintf fmt "@[unsat:%b,@;bo: @[%a@],@;citv: @[%a@],@;formula: @[%a@]@]" is_unsat BoItvs.pp bo_itvs CItvs.pp citvs Formula.pp formula -let true_ = {satisfiable= true; bo_itvs= BoItvs.empty; citvs= CItvs.empty; formula= Formula.ttrue} +let true_ = {is_unsat= false; bo_itvs= BoItvs.empty; citvs= CItvs.empty; formula= Formula.ttrue} -let false_ = {satisfiable= false; bo_itvs= BoItvs.empty; citvs= CItvs.empty; formula= Formula.ttrue} +let false_ = {is_unsat= true; bo_itvs= BoItvs.empty; citvs= CItvs.empty; formula= Formula.ttrue} -let and_nonnegative v ({satisfiable; bo_itvs; citvs; formula} as phi) = - if not satisfiable then phi +let and_nonnegative v ({is_unsat; bo_itvs; citvs; formula} as phi) = + if is_unsat then phi else - { satisfiable + { is_unsat ; bo_itvs= BoItvs.add v Itv.ItvPure.nat bo_itvs ; citvs= CItvs.add v CItv.zero_inf citvs ; formula= Formula.(aand (mk_less_equal Term.zero (Term.of_absval v)) formula) } -let and_positive v ({satisfiable; bo_itvs; citvs; formula} as phi) = - if not satisfiable then phi +let and_positive v ({is_unsat; bo_itvs; citvs; formula} as phi) = + if is_unsat then phi else - { satisfiable + { is_unsat ; bo_itvs= BoItvs.add v Itv.ItvPure.pos bo_itvs ; citvs= CItvs.add v (CItv.ge_to IntLit.one) citvs ; formula= Formula.(aand (mk_less_than Term.zero (Term.of_absval v)) formula) } -let and_eq_int v i ({satisfiable; bo_itvs; citvs; formula} as phi) = - if not satisfiable then phi +let and_eq_int v i ({is_unsat; bo_itvs; citvs; formula} as phi) = + if is_unsat then phi else - { satisfiable + { is_unsat ; bo_itvs= BoItvs.add v (Itv.ItvPure.of_int_lit i) bo_itvs ; citvs= CItvs.add v (CItv.equal_to i) citvs ; formula= Formula.(aand (mk_equal (Term.of_absval v) (Term.of_intlit i)) formula) } -let simplify ~keep {satisfiable; bo_itvs; citvs; formula} = - if not satisfiable then false_ +let simplify ~keep {is_unsat; bo_itvs; citvs; formula} = + if is_unsat then false_ else let is_in_keep v _ = AbstractValue.Set.mem v keep in - { satisfiable + let formula = Formula.simplify ~keep formula in + { is_unsat= is_unsat || Formula.is_literal_false formula ; bo_itvs= BoItvs.filter is_in_keep bo_itvs ; citvs= CItvs.filter is_in_keep citvs - ; formula= Formula.simplify ~keep formula } + ; formula } let subst_find_or_new subst addr_callee = @@ -186,7 +187,7 @@ let and_formula_callee subst formula_caller formula_callee = let and_callee subst phi ~callee:phi_callee = - if (not phi.satisfiable) || not phi_callee.satisfiable then (subst, false_) + if phi.is_unsat || phi_callee.is_unsat then (subst, false_) else match and_bo_itvs_callee subst phi.bo_itvs phi_callee.bo_itvs with | exception Contradiction -> @@ -201,9 +202,9 @@ let and_callee subst phi ~callee:phi_callee = let subst, formula' = and_formula_callee subst phi.formula phi_callee.formula in L.d_printfln "conjoined formula post call: %a@\n" Formula.pp formula' ; let formula' = Formula.normalize formula' in - let satisfiable = not (Formula.is_literal_false formula') in - if not satisfiable then L.d_printfln "contradiction found by formulas" ; - (subst, {satisfiable; bo_itvs= bo_itvs'; citvs= citvs'; formula= formula'}) ) + let is_unsat = Formula.is_literal_false formula' in + if is_unsat then L.d_printfln "contradiction found by formulas" ; + (subst, {is_unsat; bo_itvs= bo_itvs'; citvs= citvs'; formula= formula'}) ) (** {2 Operations} *) @@ -254,10 +255,10 @@ let eval_formula_binop binop_addr binop op_lhs op_rhs formula = aand (mk_equal (Term.of_absval binop_addr) t_binop) formula -let eval_binop binop_addr binop op_lhs op_rhs ({satisfiable; bo_itvs; citvs; formula} as phi) = - if not phi.satisfiable then phi +let eval_binop binop_addr binop op_lhs op_rhs ({is_unsat; bo_itvs; citvs; formula} as phi) = + if phi.is_unsat then phi else - { satisfiable + { is_unsat ; bo_itvs= eval_bo_itv_binop binop_addr binop op_lhs op_rhs bo_itvs ; citvs= eval_citv_binop binop_addr binop op_lhs op_rhs citvs ; formula= eval_formula_binop binop_addr binop op_lhs op_rhs formula } @@ -286,10 +287,10 @@ let eval_formula_unop unop_addr (unop : Unop.t) addr formula = aand (mk_equal (Term.of_absval unop_addr) t_unop) formula -let eval_unop unop_addr unop addr ({satisfiable; bo_itvs; citvs; formula} as phi) = - if not phi.satisfiable then phi +let eval_unop unop_addr unop addr ({is_unsat; bo_itvs; citvs; formula} as phi) = + if phi.is_unsat then phi else - { satisfiable + { is_unsat ; bo_itvs= eval_bo_itv_unop unop_addr unop addr bo_itvs ; citvs= eval_citv_unop unop_addr unop addr citvs ; formula= eval_formula_unop unop_addr unop addr formula } @@ -304,7 +305,7 @@ let prune_bo_with_bop ~negated v_opt arith bop arith' phi = | None -> phi | Some (_, Bottom) -> - {phi with satisfiable= false} + {phi with is_unsat= true} | Some (v, NonBottom arith_pruned) -> {phi with bo_itvs= BoItvs.add v arith_pruned phi.bo_itvs} @@ -327,10 +328,10 @@ let record_citv_abduced addr_opt arith_opt citvs = CItvs.add addr arith citvs -let bind_satisfiable phi ~f = if phi.satisfiable then f phi else phi +let bind_is_unsat phi ~f = if phi.is_unsat then phi else f phi -let prune_binop ~negated bop lhs_op rhs_op ({satisfiable; bo_itvs= _; citvs; formula} as phi) = - if not satisfiable then phi +let prune_binop ~negated bop lhs_op rhs_op ({is_unsat; bo_itvs= _; citvs; formula} as phi) = + if is_unsat then phi else let value_lhs_opt, arith_lhs_opt, bo_itv_lhs, t_lhs = eval_operand phi lhs_op in let value_rhs_opt, arith_rhs_opt, bo_itv_rhs, t_rhs = eval_operand phi rhs_op in @@ -346,38 +347,38 @@ let prune_binop ~negated bop lhs_op rhs_op ({satisfiable; bo_itvs= _; citvs; for in {phi with citvs} in - let satisfiable = + let is_unsat = match Itv.ItvPure.arith_binop bop bo_itv_lhs bo_itv_rhs |> Itv.ItvPure.to_boolean with | False -> - negated - | True -> not negated + | True -> + negated | Top -> - true - | Bottom -> false + | Bottom -> + true in - if not satisfiable then L.d_printfln "contradiction detected by inferbo intervals" ; - let phi = {phi with satisfiable} in + if is_unsat then L.d_printfln "contradiction detected by inferbo intervals" ; + let phi = {phi with is_unsat} in let phi = - bind_satisfiable phi ~f:(fun phi -> + bind_is_unsat phi ~f:(fun phi -> prune_bo_with_bop ~negated value_lhs_opt bo_itv_lhs bop bo_itv_rhs phi ) in let phi = Option.value_map (Binop.symmetric bop) ~default:phi ~f:(fun bop' -> - bind_satisfiable phi ~f:(fun phi -> + bind_is_unsat phi ~f:(fun phi -> prune_bo_with_bop ~negated value_rhs_opt bo_itv_rhs bop' bo_itv_lhs phi ) ) in - if not phi.satisfiable then phi + if phi.is_unsat then phi else let f_positive = Formula.of_term_binop bop t_lhs t_rhs in let formula = let f = if negated then Formula.nnot f_positive else f_positive in Formula.aand f formula |> Formula.normalize in - let satisfiable = not (Formula.is_literal_false formula) in - if not satisfiable then L.d_printfln "contradiction detected by formulas" ; - {phi with satisfiable; formula} + let is_unsat = Formula.is_literal_false formula in + if is_unsat then L.d_printfln "contradiction detected by formulas" ; + {phi with is_unsat; formula} (** {2 Queries} *) @@ -388,9 +389,14 @@ let is_known_zero phi v = || BoItvs.find_opt v phi.bo_itvs |> Option.value_map ~default:false ~f:Itv.ItvPure.is_zero -let is_unsat_cheap phi = (not phi.satisfiable) || Formula.is_literal_false phi.formula +let is_unsat_cheap phi = phi.is_unsat || Formula.is_literal_false phi.formula let is_unsat_expensive phi = (* note: contradictions are detected eagerly for all sub-domains except formula, so just evaluate that one *) - is_unsat_cheap phi || Formula.normalize phi.formula |> Formula.is_literal_false + if is_unsat_cheap phi then (phi, true) + else + let formula = Formula.normalize phi.formula in + let is_unsat = Formula.is_literal_false formula in + let phi = {phi with is_unsat; formula} in + (phi, is_unsat) diff --git a/infer/src/pulse/PulsePathCondition.mli b/infer/src/pulse/PulsePathCondition.mli index 55556e818..5c135928f 100644 --- a/infer/src/pulse/PulsePathCondition.mli +++ b/infer/src/pulse/PulsePathCondition.mli @@ -55,5 +55,5 @@ val is_known_zero : t -> AbstractValue.t -> bool val is_unsat_cheap : t -> bool (** whether the state contains a contradiction, call this as often as you want *) -val is_unsat_expensive : t -> bool +val is_unsat_expensive : t -> t * bool (** whether the state contains a contradiction, only call this when you absolutely have to *)