From b73b7031c5e5f272d3fad14767c9724a37f05b0e Mon Sep 17 00:00:00 2001 From: Nick Benton Date: Fri, 28 Jun 2024 05:49:10 -0700 Subject: [PATCH] [infer] Delete Formula.normalize Reviewed By: skcho Differential Revision: D58814273 fbshipit-source-id: db00efb17ed7b24228c4c526fc9e98eef0101052 --- infer/src/pulse/PulseAbductiveDomain.ml | 10 +-- infer/src/pulse/PulseFormula.ml | 101 +---------------------- infer/src/pulse/PulseFormula.mli | 3 - infer/src/pulse/PulseTopl.ml | 3 +- infer/src/pulse/unit/PulseFormulaTest.ml | 2 +- 5 files changed, 4 insertions(+), 115 deletions(-) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index be0278057b7..96516ceea63 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -1895,20 +1895,12 @@ module Summary = struct let of_post_ proc_name (proc_attrs : ProcAttributes.t) location astate0 = let open SatUnsat.Import in let astate = astate0 in - (* NOTE: we normalize (to strengthen the equality relation used by canonicalization) then - canonicalize *before* garbage collecting unused addresses in case we detect any last-minute - contradictions about addresses we are about to garbage collect *) - let* path_condition, new_eqs = Formula.normalize ~location astate.path_condition in - let astate = {astate with path_condition} in - let* astate, error = incorporate_new_eqs astate new_eqs in let astate_before_filter = astate in (* do not store the decompiler in the summary and make sure we only use the original one by marking it invalid *) let astate = {astate with decompiler= Decompiler.invalid} in let* astate, live_addresses, dead_addresses, new_eqs = filter_for_summary proc_name astate in - let+ astate, error = - match error with None -> incorporate_new_eqs astate new_eqs | Some _ -> Sat (astate, error) - in + let+ astate, error = incorporate_new_eqs astate new_eqs in match error with | None -> ( (* NOTE: it's important for correctness that we check leaks last because we are going to carry diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml index 8cf60879604..ae792312a7e 100644 --- a/infer/src/pulse/PulseFormula.ml +++ b/infer/src/pulse/PulseFormula.ml @@ -889,13 +889,6 @@ module Term = struct fold_map_direct_subterms t ~init:() ~f:(fun () t' -> ((), f t')) |> snd - let rec fold_map_subterms t ~init ~f = - let acc, t' = - fold_map_direct_subterms t ~init ~f:(fun acc t' -> fold_map_subterms t' ~init:acc ~f) - in - f acc t' - - let satunsat_map_direct_subterms t ~f = let exception FoundUnsat in try @@ -905,10 +898,6 @@ module Term = struct with FoundUnsat -> Unsat - let fold_subterms t ~init ~f = fold_map_subterms t ~init ~f:(fun acc t' -> (f acc t', t')) |> fst - - let map_subterms t ~f = fold_map_subterms t ~init:() ~f:(fun () t' -> ((), f t')) |> snd - let rec fold_subst_variables ~init ~f_subst ?(f_post = fun ~prev:_ acc t -> (acc, t)) t = match t with | Var v -> @@ -1516,14 +1505,6 @@ module Atom = struct let fold_terms atom ~init ~f = fold_map_terms atom ~init ~f:(fun acc t -> (f acc t, t)) |> fst - let fold_subterms atom ~init ~f = - fold_terms atom ~init ~f:(fun acc t -> Term.fold_subterms t ~init:acc ~f) - - - let iter_subterms atom ~f = Container.iter ~fold:fold_subterms atom ~f - - let exists_subterm atom ~f = Container.exists ~iter:iter_subterms atom ~f - let fold_variables atom ~init ~f = fold_terms atom ~init ~f:(fun acc t -> Term.fold_variables t ~init:acc ~f) @@ -1549,9 +1530,6 @@ module Atom = struct let map_terms atom ~f = fold_map_terms atom ~init:() ~f:(fun () t -> ((), f t)) |> snd - (* Preseves physical equality if [f] does. *) - let map_subterms atom ~f = map_terms atom ~f:(fun t -> Term.map_subterms t ~f) - let to_term : t -> Term.t = function | LessEqual (t1, t2) -> LessEqual (t1, t2) @@ -2262,10 +2240,6 @@ module Formula = struct val set_intervals : intervals -> t -> t - val reset_atoms : t -> t - - val reset_term_eqs : t -> t - val unsafe_mk : var_eqs:var_eqs -> const_eqs:Term.t Var.Map.t @@ -2759,12 +2733,6 @@ module Formula = struct let set_intervals intervals phi = {phi with intervals} - let reset_atoms phi = {phi with atoms= Atom.Set.empty; atoms_occurrences= Var.Map.empty} - - let reset_term_eqs phi = - {phi with term_eqs= Term.VarMap.empty; term_eqs_occurrences= Var.Map.empty} - - let unsafe_mk ~var_eqs ~const_eqs ~type_constraints ~linear_eqs ~term_eqs ~tableau ~intervals ~atoms ~linear_eqs_occurrences ~tableau_occurrences ~term_eqs_occurrences ~atoms_occurrences = @@ -4062,65 +4030,6 @@ module DynamicTypes = struct else None - let really_simplify formula = - let simplify_term (t : Term.t) = - match t with - | IsInstanceOf {var= v; typ; nullable} -> ( - match evaluate_instanceof formula v typ nullable with None -> t | Some t' -> t' ) - | t -> - t - in - let simplify_atom atom = Atom.map_subterms ~f:simplify_term atom in - let open SatUnsat.Import in - let old_atoms = formula.phi.atoms in - let* phi, new_eqs = - let f t v acc_phi = - let* acc_phi in - let t = simplify_term t in - Formula.Normalizer.and_var_term v t acc_phi - in - Formula.term_eqs_fold f formula.phi - (Sat (formula.phi |> Formula.reset_term_eqs |> Formula.reset_atoms, RevList.empty)) - in - let+ phi, new_eqs = - let f atom acc_phi = - let* acc_phi in - let atom = simplify_atom atom in - Formula.Normalizer.and_atom atom acc_phi - in - Atom.Set.fold f old_atoms (Sat (phi, new_eqs)) - in - ({formula with phi}, new_eqs) - - - let has_instanceof formula = - let in_term (t : Term.t) = match t with IsInstanceOf _ -> true | _ -> false in - let in_atom atom = Atom.exists_subterm atom ~f:in_term in - Formula.term_eqs_exists (fun t _v -> in_term t) formula.phi - || Atom.Set.exists in_atom formula.phi.atoms - - - (* The previous summary-time simplification wipes out v1 = InstanceOf(v2,t) when we can evaluate the term, which messes with - the distinction between latent and manifest errors (if v2 is an argument). I tried hacks to keep the - intensional information, but they're unconvincing and a waste of effort, since we ultimately aim to remove the simplification - phase anyway. Instead, we just log situations in which the simplification would lead to Unsat, as those are ones in which the - new on-the-fly propagation is deficient. If none show up, we can safely remove simplification. - *) - let simplify ?location formula = - if has_instanceof formula then - match really_simplify formula with - | Unsat -> - L.d_printfln ~color:Pp.Orange "WARNING: Summary-time simplify returned Unsat on %a" pp - formula ; - ScubaLogging.log_message_with_location ~label:"summary_unsat" - ~loc:(Option.value_map location ~default:"missing" ~f:Location.to_string) - ~message:"summary-time normalization returned Unsat" - | Sat _ -> - () - else () ; - Sat (formula, RevList.empty) - - (* TODO: fix messy separation between (new) InstanceOf and (old) DynamicTypes - not sure where to put the next definition *) let and_callee_type_constraints v type_constraints_foreign (phi, new_eqs) = match type_constraints_foreign with @@ -4185,13 +4094,6 @@ let and_equal_instanceof v1 v2 t ~nullable formula = Sat (formula, new_eqs') -let normalize ?location formula = - (* Sat (formula, RevList.empty) *) - Debug.p "@\n@\n***NORMALIZING NOW***@\n@\n" ; - (* normalization happens incrementally except for dynamic types (TODO) *) - DynamicTypes.simplify ?location formula - - let and_dynamic_type v t ?source_file formula = let v = (Formula.get_repr formula.phi v :> Var.t) in let tenv = PulseContext.tenv_exn () in @@ -4593,7 +4495,6 @@ end let simplify ~precondition_vocabulary ~keep formula = let open SatUnsat.Import in - let* formula, new_eqs = normalize formula in L.d_printfln_escaped "@[Simplifying %a@ wrt %a (keep),@ with prunables=%a@]" pp formula Var.Set.pp keep Var.Set.pp precondition_vocabulary ; (* get rid of as many variables as possible *) @@ -4601,7 +4502,7 @@ let simplify ~precondition_vocabulary ~keep formula = (* TODO: doing [QuantifierElimination.eliminate_vars; DeadVariables.eliminate] a few times may eliminate even more variables *) let+ formula, live_vars = DeadVariables.eliminate ~precondition_vocabulary ~keep formula in - (formula, live_vars, new_eqs) + (formula, live_vars, RevList.empty) let is_known_non_pointer formula v = Formula.is_non_pointer formula.phi v diff --git a/infer/src/pulse/PulseFormula.mli b/infer/src/pulse/PulseFormula.mli index ffd018ad048..cfc5e187923 100644 --- a/infer/src/pulse/PulseFormula.mli +++ b/infer/src/pulse/PulseFormula.mli @@ -90,9 +90,6 @@ val prune_binop : negated:bool -> Binop.t -> operand -> operand -> t -> (t * new (** {3 Operations} *) -val normalize : ?location:Location.t -> t -> (t * new_eqs) SatUnsat.t -(** think a bit harder about the formula *) - val simplify : precondition_vocabulary:Var.Set.t -> keep:Var.Set.t -> t -> (t * Var.Set.t * new_eqs) SatUnsat.t diff --git a/infer/src/pulse/PulseTopl.ml b/infer/src/pulse/PulseTopl.ml index 85634d60116..7084dd6752a 100644 --- a/infer/src/pulse/PulseTopl.ml +++ b/infer/src/pulse/PulseTopl.ml @@ -343,7 +343,6 @@ end = struct let* path_condition, new_eqs_a = Formula.prune_binop ~negated:false op l r path_condition in - let* path_condition, new_eqs_b = Formula.normalize path_condition in let new_eqs = let new_eqs = RevList.empty in let new_eqs = @@ -358,7 +357,7 @@ end = struct new_eqs in let ( ++ ) = RevList.append in - new_eqs ++ new_eqs_a ++ new_eqs_b + new_eqs ++ new_eqs_a in let* heap = let incorporate_eq heap (eq : Formula.new_eq) = diff --git a/infer/src/pulse/unit/PulseFormulaTest.ml b/infer/src/pulse/unit/PulseFormulaTest.ml index e66f91d1978..44adb791e51 100644 --- a/infer/src/pulse/unit/PulseFormulaTest.ml +++ b/infer/src/pulse/unit/PulseFormulaTest.ml @@ -192,7 +192,7 @@ let nil_typ = Typ.mk (Tstruct (ErlangType Nil)) let cons_typ = Typ.mk (Tstruct (ErlangType Cons)) -let normalize_with phi init_phi = test ~f:(fun phi -> normalize phi >>| fst) phi init_phi +let normalize_with phi init_phi = test ~f:(fun phi -> Sat phi) phi init_phi let normalize phi = normalize_with phi ttrue